Theorem RealRMK.measure_le_of_isCompact_of_integral

Modification history

2025-11-04 23:41
Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean
feat: uniqueness of measures in the Riesz–Markov–Kakutani representation theorem (#28061) …
Added RealRMK.measure_le_of_isCompact_of_integralView on Github →