Theorem MeasureTheory.tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum

Modification history

2026-01-26 08:43
Mathlib/MeasureTheory/Measure/AddContent.lean
feat: let `AddContent` take values in a general monoid (#34434) …
Modified MeasureTheory.tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsumView on Github →
2025-02-27 18:07
Mathlib/MeasureTheory/Measure/AddContent.lean
feat: a σ-additive content on a set ring is σ-subadditive (#22360) …
Added MeasureTheory.tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsumView on Github →