OAI/Geometry/NodalSets/Elliptic/CorrugationNormBounds.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Yau.Geometry.clm_apply_boundline 10 - lemma
OAI.Yau.Geometry.clm_unit_boundline 15 - lemma
OAI.Yau.Geometry.bilinear_unit_boundline 20 - lemma
OAI.Yau.Geometry.compact_second_derivative_boundline 26 - lemma
OAI.Yau.Geometry.corrugationMetricError_operator_boundline 45