English
If t is covered by a countable family of sets v(n) with finite μ-measure on each t ∩ v(n), then μ(t ∩ s) equals μ(toMeasurable μ t ∩ s) for any measurable s.
Русский
Если t ⊆ ⋃_n v(n) и μ(t ∩ v(n)) < ∞ для каждого n, тогда для любого измеримого s выполняется μ(t ∩ s) = μ(toMeasurable μ t ∩ s).
LaTeX
$$$t \subseteq \bigcup_{n} v(n) \; \land\; \forall n, μ(t \cap v(n)) < ∞ \Rightarrow μ(t \cap s) = μ(toMeasurable(μ,t) \cap s)$$$
Lean4
/-- If the union of disjoint measurable sets has finite measure, then there are only
finitely many members of the union whose measure exceeds any given positive number. -/
theorem finite_const_le_meas_of_disjoint_iUnion {ι : Type*} [MeasurableSpace α] (μ : Measure α) {ε : ℝ≥0∞}
(ε_pos : 0 < ε) {As : ι → Set α} (As_mble : ∀ i : ι, MeasurableSet (As i)) (As_disj : Pairwise (Disjoint on As))
(Union_As_finite : μ (⋃ i, As i) ≠ ∞) : Set.Finite {i : ι | ε ≤ μ (As i)} :=
finite_const_le_meas_of_disjoint_iUnion₀ μ ε_pos (fun i ↦ (As_mble i).nullMeasurableSet)
(fun _ _ h ↦ Disjoint.aedisjoint (As_disj h)) Union_As_finite
