English
For an empty diagram F, a cone c is limiting iff its cone point is terminal; i.e., IsLimit c ≃ IsTerminal c.pt.
Русский
Для пустого диаграммного индекса конус \(c\) является ограничивающим тогда и только тогда, когда точка конуса терминиальна; то есть IsLimit c ≃ IsTerminal c.pt.
LaTeX
$$$\\text{IsLimit}(c) \\simeq \\text{IsTerminal}(c.{\\rm pt})$$$
Lean4
/-- Replacing an empty cone in `IsLimit` by another with the same cone point
is an equivalence. -/
def isLimitEmptyConeEquiv (c₁ : Cone F₁) (c₂ : Cone F₂) (h : c₁.pt ≅ c₂.pt) : IsLimit c₁ ≃ IsLimit c₂
where
toFun hl := isLimitChangeEmptyCone C hl c₂ h
invFun hl := isLimitChangeEmptyCone C hl c₁ h.symm
left_inv := by dsimp [Function.LeftInverse]; intro; simp only [eq_iff_true_of_subsingleton]
right_inv := by
dsimp [Function.LeftInverse, Function.RightInverse]; intro
simp only [eq_iff_true_of_subsingleton]
