hasTerminal_iff — Mathlib

English

Two categories that are equivalent have terminal objects simultaneously: C has a terminal object iff D has a terminal object.

Русский

Две эквивалентные категории обладают терминальным объектом одновременно: в C есть терминальный объект тогда и только тогда, когда в D есть терминальный объект.

LaTeX

$$$\operatorname{HasTerminal}(C) \iff \operatorname{HasTerminal}(D)$$$

Lean4

theorem hasTerminal_iff (e : C ≌ D) : HasTerminal C ↔ HasTerminal D :=
  ⟨fun (_ : HasTerminal C) => hasTerminal_of_equivalence e.inverse, fun (_ : HasTerminal D) =>
    hasTerminal_of_equivalence e.functor⟩

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