English
Let f: α → β and s ⊆ Finite α, t ⊆ Finite β with f(a) ∈ t for all a ∈ s. Suppose that for every b ∈ t the fiber {a ∈ s | f(a) = b} has cardinality at most n. Then |s| ≤ n · |t|.
Русский
Пусть f: α → β и Пусть s — конечное подмножество α, t — конечное подмножество β, причем f(a) ∈ t для всех a ∈ s. Пусть для каждого b ∈ t множество {a ∈ s | f(a) = b} имеет кардинальность не более n. Тогда |s| ≤ n · |t|.
LaTeX
$$$\\forall f: \\alpha \\to \\beta\\,\\forall s: \\mathrm{Finset}(\\alpha)\\,\\forall t: \\mathrm{Finset}(\\beta),\\\\\n\\quad (\\forall a \\in s, f(a) \\in t) \\,\\to\\\\\n\\quad (\\forall n:\\\\mathbb{N},\\ \\forall b \\in t, \\#\\{a \\in s : f(a) = b\\} \\le n) \\,\\to\\\\\n\\quad |s| \\le n \\cdot |t|$$
Lean4
theorem card_le_mul_card_image_of_maps_to {f : α → β} {s : Finset α} {t : Finset β} (Hf : ∀ a ∈ s, f a ∈ t) (n : ℕ)
(hn : ∀ b ∈ t, #({a ∈ s | f a = b}) ≤ n) : #s ≤ n * #t :=
calc
#s = ∑ b ∈ t, #({a ∈ s | f a = b}) := card_eq_sum_card_fiberwise Hf
_ ≤ ∑ _b ∈ t, n := (sum_le_sum hn)
_ = _ := by simp [mul_comm]
