OAI/Geometry/RCD/Metric/HoleBallVolumeCover.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite hole-cover volume estimate

De Philippis--Gigli (2018), Lemma 3.3, with an explicit covering constant.

  1. theorem OAI.RegularPointCoordinates.hole_ball_volume_cover line 15