isIso_of_isDiscrete — Mathlib

English

In a discrete category with IsDiscrete, every morphism is an isomorphism; its inverse is given by reversing the underlying equality.

Русский

В дискретной категории с IsDiscrete каждый морфизм является изоморфизмом; обратный морфизм задаётся обратным равенством на основа.

LaTeX

$$$\\forall f:\\, X \\to Y,\\; IsIso(f)$$$

Lean4

instance isIso_of_isDiscrete {X Y : C} (f : X ⟶ Y) : IsIso f :=
  ⟨eqToHom (IsDiscrete.eq_of_hom f).symm, by cat_disch⟩

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