OAI/Analysis/KadisonKastler/UniformProjectionGap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform projection witnesses from modular coisometries

  1. theorem OAI.KadisonKastler.exists_projection_gap_of_finite_pinching line 18
  2. theorem OAI.KadisonKastler.exists_uniform_projection_gap line 53