mul_card_image_le_card — Mathlib

English

For a map f: α → β and a finite s ⊆ α, if for all b ∈ s.image f we have a bound on the fiber {a ∈ s | f a = b}, then n · |(s.image f)| ≥ |s|.

Русский

Пусть f: α → β и s — конечное подмножество. Если для каждого b ∈ s.image f выполнено ограничение на размер фибра {a ∈ s | f(a)=b}, то n · |s.image f| ≥ |s|.

LaTeX

$$$\\forall f: \\alpha \\to \\beta\\, \\forall s:\\mathrm{Finset}(\\alpha),\\ (\\forall b \\in s.image f,\\#\\{a \\in s \\mid f a = b\\} \\le n) \\to n \\cdot |s. image f| \\ge |s|$$

Lean4

theorem mul_card_image_le_card {f : α → β} (s : Finset α) (n : ℕ) (hn : ∀ b ∈ s.image f, n ≤ #({a ∈ s | f a = b})) :
    n * #(s.image f) ≤ #s :=
  mul_card_image_le_card_of_maps_to (fun _ ↦ mem_image_of_mem _) n hn

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