exists_lt_sum_fiber_of_nsmul_lt_sum

English

Let hf ensure f(s) ⊆ t, ht nonempty, and #t · b ≤ #s. Then there exists y ∈ t with b ≤ #{x ∈ s | f(x) = y}.

Русский

Пусть образ s лежит в t, t непусто и #t · b ≤ #s. Тогда существует y ∈ t такое, что b ≤ #{x ∈ s | f(x) = y}.

LaTeX

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

Lean4

/-- The pigeonhole principle for finitely many pigeons of different weights, strict inequality
version: there is a pigeonhole with the total weight of pigeons in it greater than `b` provided that
the total number of pigeonholes times `b` is less than the total weight of all pigeons. -/
theorem exists_lt_sum_fiber_of_nsmul_lt_sum (hb : card β • b < ∑ x, w x) : ∃ y, b < ∑ x with f x = y, w x :=
  let ⟨y, _, hy⟩ := exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum (fun _ _ => mem_univ _) hb
  ⟨y, hy⟩

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