card_biUnion_le_card_mul — Mathlib

English

For a finite set s and a function f: s → Finset β, the cardinality of the biUnion is bounded by |s| times n, whenever |f(a)| ≤ n for all a ∈ s.

Русский

Для конечного множества s и функции f: s → Finset β, кардинал biUnion ограничен как |s| · n, если для всех a ∈ s выполняется |f(a)| ≤ n.

LaTeX

$$$ \\forall s : \\mathrm{Finset} \\iota, f : \\iota \\to \\mathrm{Finset} \\beta, n : \\mathbb{N}, ( \\forall a \\in s, |f(a)| \\le n ) \\Rightarrow |s.\\mathrm{biUnion} f| \\le |s| \\cdot n. $$$

Lean4

theorem card_biUnion_le_card_mul [DecidableEq β] (s : Finset ι) (f : ι → Finset β) (n : ℕ) (h : ∀ a ∈ s, #(f a) ≤ n) :
    #(s.biUnion f) ≤ #s * n :=
  card_biUnion_le.trans <| sum_le_card_nsmul _ _ _ h

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