OAI/Geometry/RCD/Metric/HoleMassCharge.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Hole radii controlled by the mass outside the good set

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.hole_mass_charge line 12