measureReal_biUnion_finset_le — Mathlib

English

For a finite index set Finset β, and sets f(b), the real measure of their union over b in s is at most the sum of the real measures of f(b).

Русский

Для конечного индекса β и множеств f(b) выполняется μ.real(⋃_{b∈s} f(b)) ≤ ∑_{b∈s} μ.real(f(b)).

LaTeX

$$$ \\mu.real \\left( \\bigcup_{b \\in s} f(b) \\right) \\leq \\sum_{p \\in s} \\mu.real (f(p)) $$$

Lean4

theorem measureReal_biUnion_finset_le (s : Finset β) (f : β → Set α) : μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p) :=
  by
  classical
    induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ hx
    IH =>
    simp only [hx, Finset.mem_insert, iUnion_iUnion_eq_or_left, not_false_eq_true, Finset.sum_insert]
    exact (measureReal_union_le _ _).trans (by gcongr)

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