addContent_biUnion_le — Mathlib

English

For any finite index set S and functions s(i) ∈ C with i ∈ S, m(⋃_{i∈S} s(i)) ≤ ∑_{i∈S} m(s(i)).

Русский

Для конечного множества индексов S и функций s(i) ∈ C, верно m(⋃_{i∈S} s(i)) ≤ ∑_{i∈S} m(s(i)).

LaTeX

$$m(\bigcup_{i \in S} s(i)) \le \sum_{i \in S} m(s(i))$$

Lean4

theorem addContent_biUnion_le {ι : Type*} (hC : IsSetRing C) {s : ι → Set α} {S : Finset ι} (hs : ∀ n ∈ S, s n ∈ C) :
    m (⋃ i ∈ S, s i) ≤ ∑ i ∈ S, m (s i) := by
  classical
    induction S using Finset.induction with
  | empty => simp
  | insert i S hiS h =>
    rw [Finset.sum_insert hiS]
    simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
    simp only [Finset.mem_insert, forall_eq_or_imp] at hs
    refine (addContent_union_le hC hs.1 (hC.biUnion_mem S hs.2)).trans ?_
    exact add_le_add le_rfl (h hs.2)

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