OAI/Geometry/SurfaceImmersion/Primitive/PrimitivePatchRealization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The constructed local primitive data feed the exact analytic theorem, with the global rank-one metric written in the original surface variables.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SupportedPrimitivePatch.exact_metric line 30