OAI/Geometry/SurfaceImmersion/Correction/PairCurveSmoothParameter.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The chart parameter for a smooth pair curve is smooth on an actual open neighborhood, as required by the global parameter-germ extension.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothDoubleChart.smooth_pair_curve_parameter line 16