OAI/Analysis/CharacterCriterion/UltrapowerSaturation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KirchbergRordam.NormUltrapower.map_positive line 37
2. lemma OAI.KirchbergRordam.NormUltrapower.unitary_lift_of_isUnit line 44
3. lemma OAI.KirchbergRordam.NormUltrapower.isUnit_of_two_grams line 71
4. theorem OAI.KirchbergRordam.NormUltrapower.unitary_lift line 83
5. def OAI.KirchbergRordam.NormUltrapower.sequenceMap line 143
6. lemma OAI.KirchbergRordam.NormUltrapower.sequenceMap_apply line 152
7. lemma OAI.KirchbergRordam.NormUltrapower.sequenceMap_null line 154
8. def OAI.KirchbergRordam.NormUltrapower.map line 160
9. lemma OAI.KirchbergRordam.NormUltrapower.map_mk line 169
10. lemma OAI.KirchbergRordam.NormUltrapower.map_diagonal line 171
11. lemma OAI.KirchbergRordam.NormUltrapower.eventually_norm_lt line 176
12. def OAI.KirchbergRordam.Intertwining.limitHom line 189
13. lemma OAI.KirchbergRordam.Intertwining.tendsto_limitHom line 215
14. lemma OAI.KirchbergRordam.Intertwining.diagonal_tendsto line 220
15. theorem OAI.KirchbergRordam.approximate_intertwining line 237