English
For a diagram K: J ⥤ Over X and a cone t over K, t is a limit if and only if the corresponding lifted cone in C, obtained via coneEquiv, is a limit. The equivalence is given by IsLimit.ofConeEquiv coneEquiv.
Русский
Для диаграммы K: J ⥤ Over X и конуса t над K конус t максимален тогда и только тогда, когда соответствующий поднесенный конус в C, полученный через coneEquiv, является пределом. Эквивалентность задается IsLimit.ofConeEquiv coneEquiv.
LaTeX
$$$$ \text{IsLimit}(\mathrm{coneEquiv.functor.obj}(t)) \quad \text{to} \quad \text{IsLimit}(t). $$$$
Lean4
/-- A cone `t` of `K : J ⥤ Over X` is a limit if and only if the corresponding cone
`coneLift t` of `liftFromOver.obj K : WithTerminal K ⥤ C` is a limit. -/
@[simps!]
def isLimitEquiv : IsLimit (coneEquiv.functor.obj t) ≃ IsLimit t :=
IsLimit.ofConeEquiv coneEquiv
