OAI/Geometry/NodalSets/Charts/CorrugationMetricErrorRescale.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Yau.Geometry.corrugationMetricError_smul_bothline 10 - lemma
OAI.Yau.Geometry.corrugationMetricError_bound_rescaleline 18 - theorem
OAI.Yau.Geometry.corrugation_actual_bounded_regime_errorsline 37