OAI/Analysis/KadisonKastler/ProjectionStrataSynthesis.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Assembling the fixed-coordinate projection strata

  1. abbrev OAI.KadisonKastler.projectionStratumMeasure line 24
  2. abbrev OAI.KadisonKastler.ProjectionStrataSpace line 27
  3. def OAI.KadisonKastler.projectionPartitionCoordinates line 30
  4. def OAI.KadisonKastler.projectionStrataSynthesis line 36
  5. theorem OAI.KadisonKastler.projectionStrataSynthesis_range_components line 41
  6. theorem OAI.KadisonKastler.projectionStrataSynthesis_range line 62