OAI/Analysis/CharacterCriterion/Absorption.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KirchbergRordam.Intertwining.dense_pointwise_cauchy line 39
2. lemma OAI.KirchbergRordam.Intertwining.limitHom_isometry line 58
3. theorem OAI.KirchbergRordam.local_approximate_surjectivity line 71
4. theorem OAI.KirchbergRordam.isomorphism_of_ultrapower_split_and_conjugacy line 189
5. def OAI.KirchbergRordam.SeparableReduction.stage line 245
6. lemma OAI.KirchbergRordam.SeparableReduction.stage_step line 249
7. lemma OAI.KirchbergRordam.SeparableReduction.stage_mono line 251
8. lemma OAI.KirchbergRordam.SeparableReduction.stage_separable line 252
9. def OAI.KirchbergRordam.SeparableReduction.termAlgebra line 257
10. lemma OAI.KirchbergRordam.SeparableReduction.adjoin_separable line 278
11. lemma OAI.KirchbergRordam.SeparableReduction.closedAdjoin_separable line 285
12. theorem OAI.KirchbergRordam.MaxTensor.separable_maxTensor line 296
13. instance OAI.KirchbergRordam.MaxTensor.powerPack_separable line 324
14. theorem OAI.KirchbergRordam.MaxTensor.pointwise_limit_of_tensor_legs line 336
15. lemma OAI.KirchbergRordam.ultrapower_left_commutes_right line 375
16. lemma OAI.KirchbergRordam.maximal_lift_image_commutes line 390
17. theorem OAI.KirchbergRordam.maximal_absorption_of_central_half_flip line 417
18. theorem OAI.KirchbergRordam.inner_local_of_ultrapower_split_and_conjugacy line 498
19. theorem OAI.KirchbergRordam.local_approximate_surjectivity_of_dense_quotient line 553
20. theorem OAI.KirchbergRordam.quotient_isomorphism_of_ultrapower_split_and_conjugacy line 594