hasTerminal_op_of_hasInitial — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance hasTerminal_op_of_hasInitial [HasInitial C] : HasTerminal Cᵒᵖ :=
  (terminalOpOfInitial initialIsInitial).hasTerminal

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