set_ncard_biUnion_le — Mathlib

English

If t is a finite index set and each s(i) is a subset of α, then the ncard of the union over i in t is at most the sum of ncard(s(i)).

Русский

Если t — конечное множество индексов, и каждое s(i) ⊆ α, то мощность объединения равна или не превышает суммарную мощность отдельных s(i).

LaTeX

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

Lean4

theorem set_ncard_biUnion_le (t : Finset ι) (s : ι → Set α) : (⋃ i ∈ t, s i).ncard ≤ ∑ i ∈ t, (s i).ncard :=
  t.apply_union_le_sum (by simp) (Set.ncard_union_le _ _)

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