OAI/Geometry/RCD/Metric/MovingPointedCompactness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Pointed precompactness with arbitrary moving centers

The CD finite-net bound is uniform in the center. The same countable distance construction therefore applies to any sequence of centers and scales whose rescaled lower curvature is bounded below by minus one.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.moving_pointed_compactness line 19