OAI/Analysis/Commutator/CentralAtoms.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.CentralAtoms.Atom line 19
2. def OAI.Kadison.CentralAtoms.projection line 21
3. lemma OAI.Kadison.CentralAtoms.isProjection line 23
4. lemma OAI.Kadison.CentralAtoms.orthogonal line 26
5. def OAI.Kadison.CentralAtoms.part line 43
6. lemma OAI.Kadison.CentralAtoms.part_projection line 45
7. lemma OAI.Kadison.CentralAtoms.part_mem_center line 48
8. lemma OAI.Kadison.CentralAtoms.part_mul line 60
9. theorem OAI.Kadison.CentralAtoms.no_atom_below_complement line 63
10. def OAI.Kadison.CentralAtoms.IsAtomicCenter line 70
11. lemma OAI.Kadison.CentralAtoms.part_eq_one_of_atomic line 73