Theorem rieszContentAux_union

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) …
Added rieszContentAux_unionView on Github →