OAI/Geometry/SurfaceImmersion/Atlas/FixedAtlasStartingFamily.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite-point spherical preparation on a prescribed atlas. The same atlas can therefore be used for the circular boundary preparation.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.small_metric_prepared_family line 18