OAI/Geometry/NodalSets/Charts/SphereChartTransition.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Yau.Target.sphereChartCoordMap line 11
  2. def OAI.Yau.Target.sphereChartTransitionDomain line 14
  3. def OAI.Yau.Target.sphereChartTransition line 17
  4. lemma OAI.Yau.Target.sphereChartCoordMap_smooth line 20
  5. lemma OAI.Yau.Target.sphereChartCoordMap_source line 26
  6. lemma OAI.Yau.Target.sphereChartTransitionDomain_open line 30
  7. lemma OAI.Yau.Target.sphereChartTransition_smoothOn line 33
  8. lemma OAI.Yau.Target.sphereChartTransition_point line 40
  9. lemma OAI.Yau.Target.sphereChartTransition_mem line 47
  10. lemma OAI.Yau.Target.sphereChartTransition_inverse line 54
  11. lemma OAI.Yau.Target.sphereChartTransition_derivative_inverse line 62
  12. lemma OAI.Yau.Target.sphereChartTransition_jacobian_ne_zero line 76