Commit 2024-09-16 23:59 97fc480f

View on Github →

chore(VectorMeasure): drop T2Space assumption here and there (#16832)

Estimated changes

Modified Mathlib/Data/Set/Pairwise/Basic.lean

added theorem Pairwise.disjoint_extend_bot

modified theorem pairwise_disjoint_mono

modified theorem pairwise_disjoint_on

modified theorem pairwise_disjoint_on_bool

Modified Mathlib/MeasureTheory/Decomposition/SignedHahn.lean

Modified Mathlib/MeasureTheory/Measure/VectorMeasure.lean

modified theorem MeasureTheory.VectorMeasure.hasSum_of_disjoint_iUnion

modified theorem MeasureTheory.VectorMeasure.of_disjoint_iUnion

modified theorem MeasureTheory.VectorMeasure.of_disjoint_iUnion_nat