apply_union_le — Mathlib

English

Continuation of the continuity from below for unions of sequences of sets in FiniteMeasure.

Русский

Продолжение непрерывности снизу для объединения последовательностей множеств в FiniteMeasure.

LaTeX

$$Tendsto (fun i ↦ μ (Accumulate f i)) atTop (𝓝 (μ (⋃ i, f i)))$$

Lean4

theorem apply_union_le (μ : FiniteMeasure Ω) {s₁ s₂ : Set Ω} : μ (s₁ ∪ s₂) ≤ μ s₁ + μ s₂ :=
  by
  have := measure_union_le (μ := (μ : Measure Ω)) s₁ s₂
  apply (ENNReal.toNNReal_mono (by finiteness) this).trans_eq
  rw [ENNReal.toNNReal_add (by finiteness) (by finiteness), coeFn_def]

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