Theorem rieszContentAux_le

Modification history

2024-12-17 01:35
Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean
feat(MeasureTheory/Integral/RieszMarkovKakutani) prove that the Riesz content is indeed a content for `NNReal` (#18775) …
Modified rieszContentAux_leView on Github →
2023-05-22 18:01
Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean
feat: port MeasureTheory.Integral.RieszMarkovKakutani (#4195)
Added rieszContentAux_leView on Github →