card_le_card_biUnion — Mathlib

English

If s is a finite set and f: s → Finset α is such that the image are pairwise disjoint and each f(i) is nonempty, then |s| ≤ |s.biUnion f|.

Русский

Пусть s — конечное множество, f: s → Finset α таково, что образные множества попарно непересекаются и каждое f(i) непусто; тогда |s| ≤ |s.biUnion f|.

LaTeX

$$$\\forall s: Finset\\,\\forall f: s \\to Finset α,\\ (s \\to Set)(f)\\;\\text{PairwiseDisjoint} \\to (\\forall i ∈ s, (f i).Nonempty) \\\\to #s ≤ #\\left( s. biUnion f \\right)$$

Lean4

theorem card_le_card_biUnion {s : Finset ι} {f : ι → Finset α} (hs : (s : Set ι).PairwiseDisjoint f)
    (hf : ∀ i ∈ s, (f i).Nonempty) : #s ≤ #(s.biUnion f) :=
  by
  rw [card_biUnion hs, card_eq_sum_ones]
  exact sum_le_sum fun i hi ↦ (hf i hi).card_pos

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