card_range_le — Mathlib

English

For any f: α → β with α finite, the range of f has cardinality at most the cardinality of α: card(range f) ≤ card α.

Русский

Для любого f: α → β, где α конечна, образ f имеет кардинальность не более, чем кардинальность α: |range f| ≤ |α|.

LaTeX

$$$f:\alpha \to \beta$ \Rightarrow |\operatorname{range}(f)| \le |\alpha|$$

Lean4

theorem card_range_le {α β : Type*} (f : α → β) [Fintype α] [Fintype (Set.range f)] :
    Fintype.card (Set.range f) ≤ Fintype.card α :=
  Fintype.card_le_of_surjective (fun a => ⟨f a, by simp⟩) fun ⟨_, a, ha⟩ => ⟨a, by simpa using ha⟩

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