OAI/Geometry/RCD/Sobolev/BoundedEnergyDensity.lean
1 declarations, 0 contain sorry, 0 declared as axioms
A bounded measurable representative of the limiting energy density
- theorem
OAI.RegularPointCoordinates.bounded_finite_density_pointwiseline 13