English
If μ is a sum of finite measures and t has finite measure under each summand, then μ agrees with the measure of t when restricted to a Measurable t' containing t via toMeasurable.
Русский
При μ = ∑ m_n и m_n(t) < ∞, для любого измеримого s имеет место μ(toMeasurable μ t ∩ s) = μ(t ∩ s).
LaTeX
$$$\mu(\mathrm{toMeasurable}(\mu,t) \cap s) = \mu(t \cap s)$, provided $\mu = \sum m_n$ и $m_n(t) < ∞$ для всех n$$
Lean4
/-- If the union of a.e.-disjoint null-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 : ι, NullMeasurableSet (As i) μ)
(As_disj : Pairwise (AEDisjoint μ on As)) (Union_As_finite : μ (⋃ i, As i) ≠ ∞) :
Set.Finite {i : ι | ε ≤ μ (As i)} :=
ENNReal.finite_const_le_of_tsum_ne_top
(ne_top_of_le_ne_top Union_As_finite (tsum_meas_le_meas_iUnion_of_disjoint₀ μ As_mble As_disj)) ε_pos.ne'
