Theorem MeasureTheory.OuterMeasure.IsCaratheodory.biUnion_of_finite

Modification history

2025-01-21 20:44
Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
refactor(Order/Disjointed): allow arbitrary partial orders as domain (#20545)
Added MeasureTheory.OuterMeasure.IsCaratheodory.biUnion_of_finiteView on Github →