OAI/Analysis/WeakInfiniteness/ReducedOperators.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.WeakPureInfiniteness.ReducedFreeLarge line 22
2. def OAI.WeakPureInfiniteness.fullToReducedLarge line 24
3. lemma OAI.WeakPureInfiniteness.fullToReducedLarge_surjective line 27
4. def OAI.WeakPureInfiniteness.reducedLargeToOperators line 32
5. lemma OAI.WeakPureInfiniteness.reducedLargeToOperators_injective line 42
6. lemma OAI.WeakPureInfiniteness.reducedLargeToOperators_element line 46
7. def OAI.WeakPureInfiniteness.freeDiagonalWitness line 49
8. lemma OAI.WeakPureInfiniteness.freeDiagonalFunctional_witness line 52
9. lemma OAI.WeakPureInfiniteness.completion_sum line 56
10. lemma OAI.WeakPureInfiniteness.norm_freeDiagonalWitness_reduced_le line 64