OAI/Geometry/Kahler/BaseChartScale.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.PinchedHartogs.BaseConstruction.chart_small_ballline 20 - lemma
OAI.PinchedHartogs.BaseConstruction.chart_norm_deficitline 34 - lemma
OAI.PinchedHartogs.BaseConstruction.peak_chart_highline 53