OAI/Geometry/CAT0Fillings/Compactness/Coordinates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.Slicing.fullSlice_borel_sub line 17
2. lemma OAI.CAT0Fillings.Slicing.fullSlice_borel_difference_bound line 28
3. lemma OAI.CAT0Fillings.Slicing.fullSlice_cutoff_difference_bound line 43
4. def OAI.CAT0Fillings.Slicing.projectedL1 line 72
5. lemma OAI.CAT0Fillings.Slicing.dist_projectedL1 line 77
6. lemma OAI.CAT0Fillings.Slicing.projectedL1_lipschitz line 95
7. lemma OAI.CAT0Fillings.ChartGeometry.coordinate_memLp line 122
8. def OAI.CAT0Fillings.ChartGeometry.coordinateL1 line 128
9. lemma OAI.CAT0Fillings.ChartGeometry.dist_coordinateL1 line 132
10. lemma OAI.CAT0Fillings.ChartGeometry.indicator_bound line 151
11. def OAI.CAT0Fillings.ChartGeometry.isolatedL1 line 158
12. lemma OAI.CAT0Fillings.ChartGeometry.dist_isolatedL1 line 163