initialOpOfTerminal — Mathlib

English

A terminal object X in C is initial in the opposite category; i.e., IsInitial( Opposite.op X ).

Русский

Терминальный объект X в C является начальственным в противоположной категории; то есть IsInitial(Opposite.op X).

LaTeX

$$$\\text{IsInitial}(\\text{Opposite.op } X)$$$

Lean4

/-- A terminal object is initial in the opposite category. -/
def initialOpOfTerminal {X : C} (t : IsTerminal X) : IsInitial (Opposite.op X)
    where
  desc s := (t.from s.pt.unop).op
  uniq _ _ _ := Quiver.Hom.unop_inj (t.hom_ext _ _)

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