hasTerminal_of_hasInitial_op — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem hasTerminal_of_hasInitial_op [HasInitial Cᵒᵖ] : HasTerminal C :=
  (terminalUnopOfInitial initialIsInitial).hasTerminal

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