lim — Mathlib

English

A bundled version of S.asLimitCone and S.asLimit, i.e. a LimitCone for S.diagram together with its limit proof.

Русский

Объединённая версия S.asLimitCone и S.asLimit: предел конуса диаграммы S вместе с доказательством предела.

LaTeX

$$$\\mathrm{lim}(S) = \\langle S.asLimitCone, S.asLimit\\rangle$$$

Lean4

/-- A bundled version of `S.asLimitCone` and `S.asLimit`. -/
def lim : Limits.LimitCone S.diagram :=
  ⟨S.asLimitCone, S.asLimit⟩

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