exists_sum_fiber_le_of_sum_le_nsmul

English

Let s,t be finite, f: s→t with maps-to condition; there exists y ∈ t with a lower bound on the fiber size.

Русский

Пусть s,t конечны, f: s→t; существует y ∈ t с нижней границей размера фибера.

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, non-strict inequality
version: there is a pigeonhole with the total weight of pigeons in it less than or equal to `b`
provided that the total number of pigeonholes times `b` is greater than or equal to the total weight
of all pigeons. -/
theorem exists_sum_fiber_le_of_sum_le_nsmul [Nonempty β] (hb : ∑ x, w x ≤ card β • b) :
    ∃ y, ∑ x with f x = y, w x ≤ b :=
  exists_le_sum_fiber_of_nsmul_le_sum (M := Mᵒᵈ) _ hb

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