OAI/Analysis/Commutator/PartialIsometryOrder.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Kadison.PartialIsometryOrder.Link line 19
  2. lemma OAI.Kadison.PartialIsometryOrder.Link.ext line 30
  3. def OAI.Kadison.PartialIsometryOrder.Link.initial line 33
  4. def OAI.Kadison.PartialIsometryOrder.Link.final line 35
  5. lemma OAI.Kadison.PartialIsometryOrder.Link.initial_projection line 37
  6. lemma OAI.Kadison.PartialIsometryOrder.Link.final_projection line 45
  7. lemma OAI.Kadison.PartialIsometryOrder.Link.mul_initial line 53
  8. lemma OAI.Kadison.PartialIsometryOrder.Link.final_mul line 56
  9. lemma OAI.Kadison.PartialIsometryOrder.Link.norm_le_one line 58
  10. lemma OAI.Kadison.PartialIsometryOrder.Link.mul_source line 64
  11. lemma OAI.Kadison.PartialIsometryOrder.Link.target_mul line 70
  12. instance OAI.Kadison.PartialIsometryOrder.Link.(instance at line 76) line 76
  13. lemma OAI.Kadison.PartialIsometryOrder.Link.le_def line 92