exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum

English

There exists a fiber with a given image y such that its fiber sum bounds by b.

Русский

Существует фибр с образом y, сумма весов по фибре ограничена b.

LaTeX

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

Lean4

/-- The pigeonhole principle for finitely many pigeons counted by weight, non-strict inequality
version: if the total weight of a finite set of pigeons is greater than or equal to `n • b`, and
they are sorted into `n > 0` pigeonholes, then for some pigeonhole, the total weight of the pigeons
in this pigeonhole is greater than or equal to `b`. -/
theorem exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum (hf : ∀ a ∈ s, f a ∈ t) (ht : t.Nonempty)
    (hb : #t • b ≤ ∑ x ∈ s, w x) : ∃ y ∈ t, b ≤ ∑ x ∈ s with f x = y, w x :=
  exists_le_of_sum_le ht <| by simpa only [sum_fiberwise_of_maps_to hf, sum_const]

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