OAI/Geometry/SurfaceImmersion/Primitive/PrimitiveOuterGeometry.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Convert the prescribed metric's convexity and the chosen outer plateau into all geometric hypotheses of the supported primitive loop.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitive_outer_geometry line 17