mk_le_of_injective — Mathlib

English

Let f: α → β be injective. Then the cardinality of α is at most the cardinality of β.

Русский

Пусть f: α → β инъективна. Тогда мощность α не превосходит мощность β.

LaTeX

$$$$ (\\exists f:\\\\alpha \\\\to \\\\beta, \\\\mathrm{Injective}(f)) \\\\Rightarrow |\\\\alpha| \\\\le |\\\\beta| $$$$

Lean4

theorem mk_le_of_injective {α β : Type u} {f : α → β} (hf : Injective f) : #α ≤ #β :=
  ⟨⟨f, hf⟩⟩

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