OAI/Geometry/RCD/Coordinates/GeometricInputCoordinates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Coordinates under local geometric estimates

For K > 0 the same metric measure space is RCD(0,n). The local estimates transfer to that curvature bound because their curvature side conditions are automatic.

  1. theorem OAI.RegularPointCoordinates.regular_coordinates_of_geometric_inputs line 19