exists_card_fiber_lt_of_card_lt_nsmul

English

There is a non-strict inequality version: if the total weight across all holes is at least the total weight, then there exists a hole with weight at least b.

Русский

Существует нестрогая форма: если суммарный вес по всем дыркам не меньше общего веса, то найдётся дыра с весом не менее b.

LaTeX

$$$\\exists y \\in t,\\; b \\le \\sum_{x \\in s, f(x)=y} w(x)$$$

Lean4

/-- The strong pigeonhole principle for finitely many pigeons and pigeonholes. There is a pigeonhole
with at most as many pigeons as the floor of the average number of pigeons across all pigeonholes.
-/
theorem exists_card_fiber_lt_of_card_lt_nsmul (hb : ↑(card α) < card β • b) : ∃ y : β, #{x | f x = y} < b :=
  let ⟨y, _, h⟩ := Finset.exists_card_fiber_lt_of_card_lt_nsmul (f := f) hb
  ⟨y, h⟩

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