English
Let f: α → β, s ⊆ α Finset, t ⊆ β Finset. If every a ∈ s satisfies f(a) ∈ t and for each b ∈ t the fiber {a ∈ s | f(a) = b} has size at least n, then n · |t| ≤ |s|.
Русский
Пусть f: α → β, s и t — конечные множества. Если f(a) ∈ t для каждого a ∈ s и для всех b ∈ t верно, что #{a ∈ s | f(a) = b} ≥ n, то n · |t| ≤ |s|.
LaTeX
$$$\\forall f: \\alpha \\to \\beta\\, \\forall s:\\mathrm{Finset}(\\alpha)\\, \\forall t:\\mathrm{Finset}(\\beta),\\\\\n(\\forall a \\in s, f(a) \\in t) \\\\to \\\\ (\\forall b \\in t, \\#\\{a \\in s \\mid f(a)=b\\} \\ge n) \\\\to \\\\ n \\cdot |t| \\le |s|$$
Lean4
theorem mul_card_image_le_card_of_maps_to {f : α → β} {s : Finset α} {t : Finset β} (Hf : ∀ a ∈ s, f a ∈ t) (n : ℕ)
(hn : ∀ b ∈ t, n ≤ #({a ∈ s | f a = b})) : n * #t ≤ #s :=
calc
n * #t = ∑ _a ∈ t, n := by simp [mul_comm]
_ ≤ ∑ b ∈ t, #({a ∈ s | f a = b}) := (sum_le_sum hn)
_ = #s := by rw [← card_eq_sum_card_fiberwise Hf]
