OAI/Analysis/Commutator/ProjectionEquivalence.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.PartialIsometryOrder.SubEquivalent line 18
  2. def OAI.Kadison.PartialIsometryOrder.Equivalent line 21
  3. def OAI.Kadison.PartialIsometryOrder.Link.adjoint line 28
  4. lemma OAI.Kadison.PartialIsometryOrder.Link.adjoint_initial line 34
  5. lemma OAI.Kadison.PartialIsometryOrder.Link.adjoint_final line 37
  6. def OAI.Kadison.PartialIsometryOrder.Link.compFull line 40
  7. lemma OAI.Kadison.PartialIsometryOrder.Link.compFull_initial line 57
  8. lemma OAI.Kadison.PartialIsometryOrder.Link.compFull_final line 64
  9. lemma OAI.Kadison.PartialIsometryOrder.subEquivalent_of_le line 73
  10. lemma OAI.Kadison.PartialIsometryOrder.equivalent_refl line 80
  11. lemma OAI.Kadison.PartialIsometryOrder.Equivalent.symm line 88
  12. lemma OAI.Kadison.PartialIsometryOrder.Equivalent.subEquivalent line 93
  13. lemma OAI.Kadison.PartialIsometryOrder.SubEquivalent.trans line 98
  14. lemma OAI.Kadison.PartialIsometryOrder.Equivalent.trans line 105
  15. lemma OAI.Kadison.PartialIsometryOrder.factor_subEquivalent_total line 113
  16. lemma OAI.Kadison.PartialIsometryOrder.finite_subEquivalent_antisymm_of_le line 122