nonempty_iso_symm — Mathlib

English

Nonempty (X ≅ Y) is equivalent to Nonempty (Y ≅ X) (symmetry of existence of isomorphisms).

Русский

Существование изоморфизма между X и Y эквивалентно существованию изоморфизма между Y и X.

LaTeX

$$$\\forall {C} [\\mathrm{Category}(C)], \\ X,Y: C, \\ \\mathrm{Nonempty}(X \\cong Y) \\Leftrightarrow \\mathrm{Nonempty}(Y \\cong X)$$$

Lean4

theorem nonempty_iso_symm (X Y : C) : Nonempty (X ≅ Y) ↔ Nonempty (Y ≅ X) :=
  ⟨fun h => ⟨h.some.symm⟩, fun h => ⟨h.some.symm⟩⟩

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