isIsomorphic_iff_nonempty_hom — Mathlib

English

In a groupoid, X and Y are isomorphic if and only if there exists a morphism X ⟶ Y.

Русский

В группе категорий X и Y изоморфны тогда и только тогда, когда существует морфизм X → Y.

LaTeX

$$IsIsomorphic X Y \\iff Nonempty (X ⟶ Y)$$

Lean4

theorem isIsomorphic_iff_nonempty_hom {C : Type u} [Groupoid.{v} C] {X Y : C} : IsIsomorphic X Y ↔ Nonempty (X ⟶ Y) :=
  (Groupoid.isoEquivHom X Y).nonempty_congr

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