OAI/Geometry/RCD/Metric/EuclideanHoleBall.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A ball inside an open Euclidean hole with an interior boundary contact

The elementary enlargement step in De Philippis--Gigli (2018), Lemma 3.3, used for the image-volume estimate in Proposition 3.2.

  1. theorem OAI.RegularPointCoordinates.euclidean_hole_ball line 17