card_biUnion_le — Mathlib

English

The cardinality of s.biUnion t is at most the sum of the cardinalities of t(a) over a ∈ s.

Русский

Кардинальность s.biUnion t не превосходит сумму кардинальностей t(a) по a∈s.

LaTeX

$$$$\\#(s.biUnion t) \\le \\sum a \\in s, \\#(t a)$$$$

Lean4

theorem card_biUnion_le [DecidableEq M] {s : Finset ι} {t : ι → Finset M} : #(s.biUnion t) ≤ ∑ a ∈ s, #(t a) :=
  haveI := Classical.decEq ι
  Finset.induction_on s (by simp) fun a s has ih =>
    calc
      #((insert a s).biUnion t) ≤ #(t a) + #(s.biUnion t) := by rw [biUnion_insert]; exact card_union_le ..
      _ ≤ ∑ a ∈ insert a s, #(t a) := by grind

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