hasTerminal_of_equivalence — Mathlib

English

If e: D ⥤ C is an equivalence and C has a terminal object, then D also has a terminal object.

Русский

Если e: D → C является эквивалентностью и в C существует терминальный объект, то и в D существует терминальный объект.

LaTeX

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

Lean4

theorem hasTerminal_of_equivalence (e : D ⥤ C) [e.IsEquivalence] [HasTerminal C] : HasTerminal D :=
  Adjunction.hasLimitsOfShape_of_equivalence e

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