isIso_iff_bijective — Mathlib

English

In the category of types, a morphism f: X → Y is an isomorphism if and only if it is bijective.

Русский

В категории типов морфизм f: X → Y является изоморфизмом тогда и только тогда, когда она биекция.

LaTeX

$$$ \\text{IsIso } f \\;\\Leftrightarrow\\; \\text{Function.Bijective}(f) $$$

Lean4

/-- A morphism in `Type u` is an isomorphism if and only if it is bijective. -/
theorem isIso_iff_bijective {X Y : Type u} (f : X ⟶ Y) : IsIso f ↔ Function.Bijective f :=
  Iff.intro (fun _ => (asIso f : X ≅ Y).toEquiv.bijective) fun b => (Equiv.ofBijective f b).toIso.isIso_hom

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