OAI/Geometry/RCD/Metric/RescaledCompactRepresentative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compact Lipschitz representatives at the original physical scale

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.rescaled_compact_representative line 13