OAI/Geometry/RCD/Metric/PointedLiftDistances.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Distances of convergent lifts in the prescribed physical scales
- theorem
OAI.RegularPointCoordinates.pointed_lift_distance_tendstoline 13