English
Let f: α → β be any map and s a finite subset of α. If n is a natural number such that for every b in the image s.image f, the fiber {a ∈ s | f(a) = b} has size at most n, then |s| ≤ n · |s.image f|.
Русский
Пусть f: α → β, s ⊆ α - конечное. Если существует натуральное число n, такое что для каждого b∈f(s) выполняется #{a∈s | f(a)=b} ≤ n, то |s| ≤ n · |f(s)|.
LaTeX
$$$\\forall f: \\alpha \\to \\beta\\, \\forall s:\\mathrm{Finset}(\\alpha),\\ \\forall n:\\mathbb{N},\\ \n(\\forall b \\in s.\\image f,\\#\\{a\\in s \\mid f a = b\\} \\le n) \\\\to \\\\ \\,|s| \\le n \\,\\cdot \\,|s. image f|$$
Lean4
theorem card_le_mul_card_image {f : α → β} (s : Finset α) (n : ℕ) (hn : ∀ b ∈ s.image f, #({a ∈ s | f a = b}) ≤ n) :
#s ≤ n * #(s.image f) :=
card_le_mul_card_image_of_maps_to (fun _ ↦ mem_image_of_mem _) n hn
