Theorems · Theorem · combinatorics

Finset.exists_card_fiber_le_of_card_le_mul

∀ {α : Type u} {β : Type v} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {n : ℕ},
  t.Nonempty → s.card ≤ t.card * n → ∃ y ∈ t, {x ∈ s | f x = y}.card ≤ n

The pigeonhole principle for finitely many pigeons counted by heads: given a function f, a finite sets s in its domain, a finite set t in its codomain, and a natural number n such that #s ≤ #t * n, there exists y ∈ t such that its preimage in s has no more than n elements. See also Finset.exists_card_fiber_lt_of_card_lt_mul for a stronger statement.

Defined in

Mathlib.Combinatorics.Pigeonhole

Cited by

0 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEq