hasLimit — Mathlib

English

For every j, the limit projection map is a linear map and respects addition and scalar action.

Русский

Для каждого j проекция предела является линейным отображением и сохраняет сложение и умножение на скаляр.

LaTeX

$$$\lim\pi_j: \mathrm{Types.Small.limitCone}(F).pt \to F(j)$ линейно по $R$ и сохраняет сложение.$$

Lean4

/-- If `(F ⋙ forget (ModuleCat R)).sections` is `u`-small, `F` has a limit. -/
instance hasLimit : HasLimit F :=
  HasLimit.mk
    { cone := limitCone F
      isLimit := limitConeIsLimit F }

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