OAI/Geometry/RCD/Coordinates/NormalizedDistanceSourceLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Vanishing normalized distance-source mass from equal volume limits

  1. theorem OAI.RegularPointCoordinates.radial_mass_normalized_tendsto_zero line 12