OAI/Analysis/Commutator/OrthogonalLinkFamily.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.PartialIsometryOrder.OrthogonalLinks line 21
2. lemma OAI.Kadison.PartialIsometryOrder.exists_maximal_orthogonalLinks line 24
3. def OAI.Kadison.PartialIsometryOrder.familySpace line 36
4. instance OAI.Kadison.PartialIsometryOrder.(instance at line 39) line 39
5. lemma OAI.Kadison.PartialIsometryOrder.familySpace_generator line 42
6. lemma OAI.Kadison.PartialIsometryOrder.familySpace_invariant line 46
7. lemma OAI.Kadison.PartialIsometryOrder.familySpace_projection_mem line 62
8. lemma OAI.Kadison.PartialIsometryOrder.familySpace_projection_mul line 73
9. lemma OAI.Kadison.PartialIsometryOrder.familySpace_target_mul line 78
10. theorem OAI.Kadison.PartialIsometryOrder.maximal_family_spans line 96