OAI/Geometry/RCD/Coordinates/VanishingRadiusCost.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Shrinking endpoint balls while their normalized error cost vanishes

  1. theorem OAI.RegularPointCoordinates.exists_vanishing_radius_cost line 13