surjective_of_injective — Mathlib

English

If α is finite and f: α → α is injective, then f is surjective.

Русский

Если α конечен и f: α → α инъективно отображает, то оно сюръективно.

LaTeX

$$$\\operatorname{Injective}(f) \\Rightarrow \\operatorname{Surjective}(f)$$$

Lean4

theorem surjective_of_injective {f : α → α} (hinj : Injective f) : Surjective f :=
  by
  intro x
  have := Classical.propDecidable
  cases nonempty_fintype α
  have h₁ : image f univ = univ :=
    eq_of_subset_of_card_le (subset_univ _) ((card_image_of_injective univ hinj).symm ▸ le_rfl)
  have h₂ : x ∈ image f univ := h₁.symm ▸ mem_univ x
  obtain ⟨y, h⟩ := mem_image.1 h₂
  exact ⟨y, h.2⟩

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