OAI/Analysis/KadisonKastler/LiftedRankStrata.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Rank strata in the universe of the original Hilbert space

  1. def OAI.KadisonKastler.rankFiberLift line 29
  2. def OAI.KadisonKastler.commonRankStratum line 33
  3. def OAI.KadisonKastler.commonRankStratumEquiv line 55
  4. def OAI.KadisonKastler.liftedRankCoordinates line 61
  5. def OAI.KadisonKastler.liftedRankRepresentation line 64
  6. theorem OAI.KadisonKastler.liftedRankRepresentation_measurable line 70