OAI/Analysis/KadisonKastler/TwoStateCornerSupports.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The quadratic off-diagonal isometry between the two state corners

  1. def OAI.KadisonKastler.twoStateEntry line 18
  2. theorem OAI.KadisonKastler.twoStateEntry_mul line 21
  3. theorem OAI.KadisonKastler.twoStateEntry_star line 25
  4. theorem OAI.KadisonKastler.twoStateEntry_fst line 32
  5. theorem OAI.KadisonKastler.twoStateEntry_snd line 41
  6. theorem OAI.KadisonKastler.twoStateCorner_rangeProjection line 52
  7. theorem OAI.KadisonKastler.twoStateSummand_mem_commutant line 77
  8. theorem OAI.KadisonKastler.twoStateSummand_reference line 90
  9. theorem OAI.KadisonKastler.twoStateEntry_projection_conjugation line 110
  10. theorem OAI.KadisonKastler.twoStateEntry_quadratic_initial line 124
  11. theorem OAI.KadisonKastler.twoStateEntry_quadratic_final line 140