hasInitial_of_hasTerminal_op — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem hasInitial_of_hasTerminal_op [HasTerminal Cᵒᵖ] : HasInitial C :=
  (initialUnopOfTerminal terminalIsTerminal).hasInitial

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