OAI/Geometry/NodalSets/Charts/ChartFrameSmooth.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Yau.Target.sphereChartDerivative_eq_fderiv line 13
  2. lemma OAI.Yau.Target.sphereChartDerivative_smooth_at line 19
  3. lemma OAI.Yau.Target.sphereChartFrame_smooth_at line 26
  4. lemma OAI.Yau.Target.circleChartDerivative_eq_fderiv line 33
  5. lemma OAI.Yau.Target.circleChartDerivative_smooth_at line 39
  6. lemma OAI.Yau.Target.circleChartFactor_smooth_at line 46
  7. lemma OAI.Yau.Target.circleChartDensity_smooth_at line 55