OAI/Analysis/KadisonKastler/CountableFiberGap.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A common conull set for the fiber gap estimate

Countably many fiber approximants, with vanishing numerical slack, bound the full fiber gap. Strong unit-ball density and weak compactness supply the passage from test fields to arbitrary contractions.

  1. theorem OAI.KadisonKastler.StrongUnitBallTestSequence.weakUnitBallDense line 23
  2. theorem OAI.KadisonKastler.kkDistance_le_of_countable_approximants line 38
  3. theorem OAI.KadisonKastler.ae_kkDistance_le_of_countable_approximants line 57