exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to

English

There exists a fiber with cardinality greater than a threshold, under the pigeonhole framing.

Русский

Существование фибра с размером больше заданного порога по кармановому принципу.

LaTeX

$$$\\exists y ∈ t, n < \\#\\{ x ∈ s | f x = y \\}$$$

Lean4

/-- The pigeonhole principle for finitely many pigeons counted by heads: there is a pigeonhole with
at least as many pigeons as the ceiling of the average number of pigeons across all pigeonholes. -/
theorem exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to (hf : ∀ a ∈ s, f a ∈ t) (ht : #t • b < #s) :
    ∃ y ∈ t, b < #({x ∈ s | f x = y}) := by
  simp_rw [cast_card] at ht ⊢
  exact exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum hf ht

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