apply_iUnion_le — Mathlib

English

Let μ be a probability measure and f_n ⊆ Ω be a sequence of sets with Summable μ(f_n). Then μ(⋃ f_n) ≤ ∑ μ(f_n).

Русский

Пусть μ – вероятность на Ω и f_n ⊆ Ω последовательность множеств с суммируемыми μ(f_n). Тогда μ(⋃_n f_n) ≤ ∑_n μ(f_n).

LaTeX

$$$\\mu\\left(\\bigcup_{n} f(n)\\right) \\le \\sum^{\\prime}_{n} \\mu(f(n))$$$

Lean4

theorem apply_iUnion_le {μ : ProbabilityMeasure Ω} {f : ℕ → Set Ω} (hf : Summable fun n ↦ μ (f n)) :
    μ (⋃ n, f n) ≤ ∑' n, μ (f n) := by
  simpa [← ENNReal.coe_le_coe, ENNReal.coe_tsum hf] using MeasureTheory.measure_iUnion_le f

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