OAI/Geometry/NodalSets/Charts/FiniteChartDerivativeSeminorm.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Yau.Geometry.finiteChartDerivativeSize_zeroline 12 - lemma
OAI.Yau.Geometry.finiteChartDerivativeSize_smul_leline 18 - lemma
OAI.Yau.Geometry.finiteChartDerivativeSize_smulline 28 - lemma
OAI.Yau.Geometry.finiteChartDerivativeSize_mono_orderline 41