hasInitial_op_of_hasTerminal — Mathlib

English

If a category C has a terminal object, then its opposite category C^op has an initial object.

Русский

Если в категории C существует терминальный объект, то в противоположной категории C^op существует начальный объект.

LaTeX

$$$\HasTerminal(C) \Rightarrow \HasInitial(C^{op}).$$$

Lean4

instance hasInitial_op_of_hasTerminal [HasTerminal C] : HasInitial Cᵒᵖ :=
  (initialOpOfTerminal terminalIsTerminal).hasInitial

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