OAI/Geometry/RCD/Coordinates/NearRegularDistanceSources.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Vanishing actual distance sources near a regular point

The absolute volume limits are constructed from regularity, rather than assumed for the selected centers and radii.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.regular_moving_distance_sources line 18