OAI/Analysis/JiangSu/DimensionDrop/DimensionDropFiberSections.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JiangSuConstruction.endpoints_ne line 17
2. def OAI.JiangSuConstruction.fiberSection line 22
3. def OAI.JiangSuConstruction.fiberBound line 49
4. lemma OAI.JiangSuConstruction.fiberBound_nonneg line 50
5. lemma OAI.JiangSuConstruction.fiberSection_tensor_bound line 52