injective_iff_surjective — Mathlib

English

On a finite type α, a function f: α → α is injective if and only if it is bijective.

Русский

На конечном типе α функция f: α → α инъективна тогда и только тогда, когда она биективна.

LaTeX

$$Injective f ↔ Bijective f$$

Lean4

theorem injective_iff_surjective {f : α → α} : Injective f ↔ Surjective f :=
  ⟨surjective_of_injective, fun hsurj =>
    HasLeftInverse.injective
      ⟨surjInv hsurj,
        leftInverse_of_surjective_of_rightInverse (surjective_of_injective (injective_surjInv _))
          (rightInverse_surjInv _)⟩⟩

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