OAI/Geometry/SurfaceImmersion/Primitive/SupportedPrimitiveGeometry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The local primitive normal bound and exterior C2 proximity together preserve immersion and a nonzero second form on the entire surface.

  1. lemma OAI.ClosedSurfaceR4.coordinateMap_eventuallyEq_at line 18
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.planeRead_eventuallyEq_on_weight line 36
  3. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData.supported_primitive_geometry line 55