OAI/Geometry/RCD/Metric/BoundedFiniteDensity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The bounded real density of a dominated finite energy limit

  1. theorem OAI.RegularPointCoordinates.bounded_finite_density line 14