equivOfIso — Mathlib

English

If X is isomorphic to Y, then X is terminal iff Y is terminal.

Русский

Если X изоморфен Y, то X терминален тогда и только тогда, когда Y терминален.

LaTeX

$$$\mathrm{IsTerminal}(X) \simeq \mathrm{IsTerminal}(Y)$ under an isomorphism$$

Lean4

/-- If `X` and `Y` are isomorphic, then `X` is terminal iff `Y` is. -/
def equivOfIso {X Y : C} (e : X ≅ Y) : IsTerminal X ≃ IsTerminal Y
    where
  toFun h := IsTerminal.ofIso h e
  invFun h := IsTerminal.ofIso h e.symm
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _

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