OAI/Geometry/SurfaceImmersion/Primitive/LocalIntrinsicCrossing.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Intrinsic curvature and ordered crossings depend only on the local smooth germ. This applies the radial calculation in an actual chart.

  1. lemma OAI.ClosedSurfaceR4.RealModes.realMetric_eventuallyEq line 13
  2. lemma OAI.ClosedSurfaceR4.RealModes.scalarDeriv_eventuallyEq line 18
  3. lemma OAI.ClosedSurfaceR4.RealModes.coordinateGauss_congr_germ line 22
  4. lemma OAI.ClosedSurfaceR4.RealModes.inducedCurvature_congr_germ line 36
  5. lemma OAI.ClosedSurfaceR4.RealModes.coordinateGaussianCurvature_pure_radial_on line 45
  6. lemma OAI.ClosedSurfaceR4.RealModes.orderedCrossing_intrinsic_pure_radial_on line 66