hasLimit_iff_hasTerminal_cone — Mathlib

English

A functor F has a limit if and only if the cone over F is terminal; i.e., HasLimit F is equivalent to HasTerminal (Cone F).

Русский

Существование предела для F эквивалентно тому, что конус над F является терминальным; HasLimit F эквивалентен HasTerminal (Cone F).

LaTeX

$$$\\text{HasLimit}(F) \\iff \\text{HasTerminal}(\\text{Cone}(F))$$$

Lean4

theorem hasLimit_iff_hasTerminal_cone (F : J ⥤ C) : HasLimit F ↔ HasTerminal (Cone F) :=
  ⟨fun _ => (Cone.isLimitEquivIsTerminal _ (limit.isLimit F)).hasTerminal, fun h =>
    haveI : HasTerminal (Cone F) := h
    ⟨⟨⟨⊤_ _, (Cone.isLimitEquivIsTerminal _).symm terminalIsTerminal⟩⟩⟩⟩

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