OAI/Geometry/RCD/Sobolev/InteriorSmoothTestBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Fixed metric bounds for the interior smooth test class

  1. theorem OAI.RegularPointCoordinates.InteriorSmoothTest.metric_bounds line 13