OAI/Analysis/KadisonKastler/TwoRatioRemoteComplement.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Finite complements for remote product blocks

  1. def OAI.KadisonKastler.twoRatioComplementSites line 13
  2. theorem OAI.KadisonKastler.mem_twoRatioComplementSites line 18
  3. theorem OAI.KadisonKastler.twoRatioComplementSites_nodup line 23
  4. theorem OAI.KadisonKastler.twoRatioComplementSites_disjoint line 27
  5. def OAI.KadisonKastler.twoRatioComplementSize line 36
  6. def OAI.KadisonKastler.PointedMatrixSites.twoRatioComplementMatrix line 46
  7. theorem OAI.KadisonKastler.PointedMatrixSites.twoRatioComplementMatrix_algebra line 51
  8. theorem OAI.KadisonKastler.PointedMatrixSites.twoRatioComplementMatrix_commutes line 57
  9. theorem OAI.KadisonKastler.PointedMatrixSites.twoRatioComplementMatrix_contains_stage line 67
  10. theorem OAI.KadisonKastler.PointedMatrixSites.twoRatioComplementMatrix_moment line 91