OAI/Analysis/Commutator/ConcreteCornerVonNeumann.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Kadison.ConcreteCorner.closedCarrier line 23
  2. abbrev OAI.Kadison.ConcreteCorner.Algebra line 28
  3. def OAI.Kadison.ConcreteCorner.inclusion line 30
  4. lemma OAI.Kadison.ConcreteCorner.inclusion_apply line 32
  5. lemma OAI.Kadison.ConcreteCorner.inclusion_injective line 34
  6. lemma OAI.Kadison.ConcreteCorner.inclusion_range line 36
  7. abbrev OAI.Kadison.ConcreteCorner.Space line 42
  8. abbrev OAI.Kadison.ConcreteCorner.representation line 44
  9. abbrev OAI.Kadison.ConcreteCorner.project line 46
  10. lemma OAI.Kadison.ConcreteCorner.project_apply line 48
  11. lemma OAI.Kadison.ConcreteCorner.representation_project line 50
  12. lemma OAI.Kadison.ConcreteCorner.representation_injective line 55
  13. def OAI.Kadison.ConcreteCorner.lift line 63
  14. lemma OAI.Kadison.ConcreteCorner.lift_apply line 66
  15. lemma OAI.Kadison.ConcreteCorner.project_fixed line 69
  16. lemma OAI.Kadison.ConcreteCorner.lift_left line 72
  17. lemma OAI.Kadison.ConcreteCorner.lift_right line 76
  18. lemma OAI.Kadison.ConcreteCorner.commutant_preserves line 84
  19. def OAI.Kadison.ConcreteCorner.restrictCommutant line 91
  20. lemma OAI.Kadison.ConcreteCorner.restrictCommutant_apply line 93
  21. lemma OAI.Kadison.ConcreteCorner.project_commutant line 95
  22. lemma OAI.Kadison.ConcreteCorner.restrictCommutant_centralizer line 100
  23. lemma OAI.Kadison.ConcreteCorner.lift_commutes line 109
  24. lemma OAI.Kadison.ConcreteCorner.lift_mem line 118
  25. lemma OAI.Kadison.ConcreteCorner.corner_bicommutant line 125
  26. def OAI.Kadison.ConcreteCorner.vonNeumann line 139
  27. lemma OAI.Kadison.ConcreteCorner.vonNeumann_range line 146