OAI/Geometry/RCD/Harmonic/FirstOrderMetricCompactness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A metric limit and the actual first-order coordinate limits together

Centers and physical radii may both vary. The metric space and its approximations are constructed from CD finite nets; the finite coordinate family is transferred through those same maps. No curvature-dimension or harmonicity assertion about the limit is assumed here.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.first_order_metric_compactness line 21