card_le_of_injective — Mathlib

English

Let α and β be finite types and f: α → β be injective. Then the cardinality of α is at most the cardinality of β: |α| ≤ |β|.

Русский

Пусть α и β — конечные множества, f: α → β инъективна. Тогда кардинальность α не превосходит кардинальности β: |α| ≤ |β|.

LaTeX

$$$f:\alpha \to \beta$ injective \Rightarrow |\alpha| \le |\beta|$$

Lean4

theorem card_le_of_injective (f : α → β) (hf : Function.Injective f) : card α ≤ card β :=
  Finset.card_le_card_of_injOn f (fun _ _ => Finset.mem_univ _) fun _ _ _ _ h => hf h

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