OAI/Geometry/SurfaceImmersion/Primitive/PrimitiveAmplitudeZero.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Outside its original chart support the actual amplitude has zero first jet.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.correctedAmplitude_zero_coordinate line 15