tsum_meas_le_meas_iUnion_of_disjoint

English

For As : ι → Set α with pairwise disjoint on As, and ∀ i, MeasurableSet (As i), we have (∑' i, μ(As i)) ≤ μ(⋃ i, As i).

Русский

Пусть As — семейство множеств, попарно непересекающихся, и каждое As(i) измеримо; тогда сумма мер по As не превышает меру их объединения.

LaTeX

$$$$ \\sum\\nabla i, \\mu(As_i) \\le \\mu\\left(\\bigcup_{i} As_i\\right). $$$$

Lean4

/-- The measure of a disjoint union (even uncountable) of measurable sets is at least the sum of
the measures of the sets. -/
theorem tsum_meas_le_meas_iUnion_of_disjoint {ι : Type*} {_ : MeasurableSpace α} (μ : Measure α) {As : ι → Set α}
    (As_mble : ∀ i : ι, MeasurableSet (As i)) (As_disj : Pairwise (Disjoint on As)) :
    (∑' i, μ (As i)) ≤ μ (⋃ i, As i) :=
  tsum_meas_le_meas_iUnion_of_disjoint₀ μ (fun i ↦ (As_mble i).nullMeasurableSet)
    (fun _ _ h ↦ Disjoint.aedisjoint (As_disj h))

Похожие утверждения