OAI/Analysis/Kaplansky/Ultrapower/PartialIsometry.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyConsequences.IsPartialIsometry line 12
2. lemma OAI.KaplanskyConsequences.IsPartialIsometry.star_op line 15
3. lemma OAI.KaplanskyConsequences.IsPartialIsometry.initial line 18
4. lemma OAI.KaplanskyConsequences.IsPartialIsometry.final line 23
5. lemma OAI.KaplanskyConsequences.IsPartialIsometry.norm_le line 25
6. lemma OAI.KaplanskyConsequences.IsPartialIsometry.zero line 29
7. lemma OAI.KaplanskyConsequences.IsPartialIsometry.of_initial line 30
8. lemma OAI.KaplanskyConsequences.IsPartialIsometry.mul_initial line 38
9. lemma OAI.KaplanskyConsequences.IsPartialIsometry.final_mul line 40
10. lemma OAI.KaplanskyConsequences.IsPartialIsometry.mul_initial_compl line 41
11. lemma OAI.KaplanskyConsequences.IsPartialIsometry.final_compl_mul line 43
12. lemma OAI.KaplanskyConsequences.IsPartialIsometry.initial_compl_mul_star line 45
13. lemma OAI.KaplanskyConsequences.IsPartialIsometry.star_mul_final_compl line 47
14. lemma OAI.KaplanskyConsequences.IsPartialIsometry.add_orthogonal line 50
15. lemma OAI.KaplanskyConsequences.IsPartialIsometry.initial_of_factor line 59