hasLimit — Mathlib

English

The constructed limit cone for F is indeed a limit cone in SemiRingCat; i.e., it satisfies the universal property of a limit.

Русский

Построенный пределный конус для F действительно является пределом в SemiRingCat; т.е. удовлетворяет универсальному свойству предела.

LaTeX

$$$\text{IsLimit} (\text{limitCone } F)$$$

Lean4

/-- If `(F ⋙ forget SemiRingCat).sections` is `u`-small, `F` has a limit. -/
instance hasLimit : HasLimit F :=
  ⟨limitCone.{v, u} F, limitConeIsLimit.{v, u} F⟩

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