OAI/Analysis/JiangSu/Comparison/FamilyRanks.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectComparison.family_isOpen_lt_rank line 19
2. lemma OAI.DirectComparison.family_isOpen_lt_realRank line 31
3. theorem OAI.DirectComparison.family_uniform_positive_cut line 47
4. theorem OAI.DirectComparison.family_scalar_almost_projection_step line 79