OAI/Analysis/Commutator/OrthogonalLinkSums.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.PartialIsometryOrder.finiteProjection line 24
2. lemma OAI.Kadison.PartialIsometryOrder.family_cross line 28
3. lemma OAI.Kadison.PartialIsometryOrder.family_final_cross line 31
4. lemma OAI.Kadison.PartialIsometryOrder.finiteProjection_projection line 37
5. lemma OAI.Kadison.PartialIsometryOrder.finiteProjection_norm_le line 52
6. lemma OAI.Kadison.PartialIsometryOrder.finiteProjection_mem line 56
7. lemma OAI.Kadison.PartialIsometryOrder.finiteProjection_mul_val line 59
8. lemma OAI.Kadison.PartialIsometryOrder.finiteProjection_target line 69
9. lemma OAI.Kadison.PartialIsometryOrder.finiteProjection_tendsto_generator line 76
10. lemma OAI.Kadison.PartialIsometryOrder.finiteProjection_tendsto_space line 84
11. theorem OAI.Kadison.PartialIsometryOrder.finiteProjection_tendsto line 104