OAI/Analysis/KadisonKastler/CentralSupportCover.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

An orthogonal family of initial projections equivalent to subprojections of e fills the central support of e. This is the geometric step in the localized row-averaging proof; no countability is imposed.

  1. def OAI.KadisonKastler.IsCentralSupportFamily line 18
  2. theorem OAI.KadisonKastler.exists_maximal_centralSupportFamily line 22
  3. theorem OAI.KadisonKastler.centralSupportFamily_fills line 36
  4. theorem OAI.KadisonKastler.exists_centralSupportCover line 83