CoordinateC1Bounds.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Fixed atlas seminorms control ordinary values and first derivatives on all the original compact chart supports.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.coordinate_C1_bound line 18