OAI/Geometry/RCD/Metric/CoarseFineImageHoleVolume.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The image-hole estimate for the actual coarse and fine coordinate data

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.coarse_fine_image_hole_volume line 14