`OAI/Geometry/RCD/Coordinates/RegularCoreRepresentative.lean`

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bounded compact Lipschitz representatives of the actual regular core

theorem OAI.RegularPointCoordinates.regular_core_representative line 15