English
Given a FiniteSpanningSetsIn S, there is a disjointed version whose underlying sets are pairwise disjoint and still spans the same family.
Русский
Для данного множества конечных охватывающих множеств существует версия с попарно непересекающимися подмножествами, которые по-прежнему образуют ту же семантику.
LaTeX
$$$S\text{ disjointed}$ is a FiniteSpanningSetsIn such that $\{S_i\}$ are pairwise disjoint and $\bigcup_i S_i$ covers the same family$$
Lean4
/-- Given `S : μ.FiniteSpanningSetsIn {s | MeasurableSet s}`,
`FiniteSpanningSetsIn.disjointed` provides a `FiniteSpanningSetsIn {s | MeasurableSet s}`
such that its underlying sets are pairwise disjoint. -/
protected def disjointed {μ : Measure α} (S : μ.FiniteSpanningSetsIn {s | MeasurableSet s}) :
μ.FiniteSpanningSetsIn {s | MeasurableSet s} :=
⟨disjointed S.set, MeasurableSet.disjointed S.set_mem, fun n =>
lt_of_le_of_lt (measure_mono (disjointed_subset S.set n)) (S.finite _), S.spanning ▸ iUnion_disjointed⟩
