OAI/Geometry/SurfaceImmersion/Atlas/GenericCoordinateLevels.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Generic common levels for finitely many radius functions in countably many surface charts. This is the radius-selection step of the global preparation.

  1. abbrev OAI.ClosedSurfaceR4.PublishedInputs.DistinctRadiusPairs line 13
  2. abbrev OAI.ClosedSurfaceR4.PublishedInputs.DistinctRadiusTriples line 14
  3. theorem OAI.ClosedSurfaceR4.PublishedInputs.exists_generic_coordinate_levels line 17