OAI/Geometry/SurfaceImmersion/Primitive/PrimitivePatchBoundary.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Transfer the actual old boundary invariant to the new analytic patch. The source restriction preserves the current primitive's vertical direction.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SupportedPrimitivePatch.current_second line 24
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SupportedPrimitivePatch.zero_amplitude_frontier line 40
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SupportedPrimitivePatch.old_boundary_crossing line 51