set_encard_biUnion_le — Mathlib

English

If t is a finite set of indices and the family s(i) is pairwise disjoint, then the encard of the union is at most the sum of encards.

Русский

Если t — конечное множество индексов и семейство s(i) попарно непересекается, то encard объединения не превосходит суммы encard.

LaTeX

$$$(\\bigcup_{i \\in t} s(i)).encard \\le \\sum_{i \\in t} (s(i)).encard$$

Lean4

theorem set_encard_biUnion_le (t : Finset ι) (s : ι → Set α) : (⋃ i ∈ t, s i).encard ≤ ∑ i ∈ t, (s i).encard :=
  t.apply_union_le_sum (by simp) (Set.encard_union_le _ _)

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