OAI/Geometry/NodalSets/Charts/RoundChartConnection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Yau.Target.ambientRoundBilinear line 13
  2. def OAI.Yau.Target.roundChartMetric line 15
  3. lemma OAI.Yau.Target.roundChartMetric_apply line 18
  4. lemma OAI.Yau.Target.roundChartMetric_center line 21
  5. lemma OAI.Yau.Target.roundChartMetric_smooth line 27
  6. lemma OAI.Yau.Target.roundChartMetric_derivative_zero line 39
  7. lemma OAI.Yau.Target.roundChartMetric_connection_zero line 51
  8. lemma OAI.Yau.Target.centeredSphereIsometry_exists line 60