OAI/Analysis/WeakInfiniteness/UniversalFreeEmbedding.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.WeakPureInfiniteness.ContractionRepresentation line 19
2. def OAI.WeakPureInfiniteness.ContractionAmbient line 27
3. instance OAI.WeakPureInfiniteness.(instance at line 30) line 30
4. instance OAI.WeakPureInfiniteness.(instance at line 34) line 34
5. def OAI.WeakPureInfiniteness.universalOperator line 38
6. def OAI.WeakPureInfiniteness.universalContractionSubalgebra line 43
7. def OAI.WeakPureInfiniteness.UniversalContraction line 46
8. instance OAI.WeakPureInfiniteness.(instance at line 48) line 48
9. def OAI.WeakPureInfiniteness.universalContractionGenerator line 50
10. def OAI.WeakPureInfiniteness.contractionEvaluation line 53
11. lemma OAI.WeakPureInfiniteness.contractionEvaluation_star line 64
12. lemma OAI.WeakPureInfiniteness.contractionEvaluation_smul line 68
13. lemma OAI.WeakPureInfiniteness.contractionEvaluation_generator line 72
14. lemma OAI.WeakPureInfiniteness.norm_universalContractionGenerator_le_one line 75