`OAI/Geometry/RCD/Coordinates/FixedGaugeRegularGradient.lean`

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform local gradient bounds for every fixed-gauge realization

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.fixed_gauge_gradient_bound line 17