OAI/Geometry/CAT0Fillings/Density/NearEuclidean.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CAT0Fillings.ChartGeometry.chart_controls_totalline 19 - lemma
OAI.CAT0Fillings.ChartGeometry.exists_positive_integer_regionline 32 - lemma
OAI.CAT0Fillings.ChartGeometry.exists_positive_near_hilbert_pieceline 74