Theorem Directed.measure_iUnion

Modification history

2026-08-20 12:42

Mathlib/MeasureTheory/Measure/Continuity.lean

chore: split too long file Measure.MeasureSpace (#42949) …

Modified Directed.measure_iUnion View on Github →

2024-09-18 11:42

Mathlib/MeasureTheory/Measure/MeasureSpace.lean

feat(MeasureTheory): generalize `measure_iUnion_eq_iSup` (#16390)

Added Directed.measure_iUnion View on Github →