lim

Mathlib.Topology.Category.Profinite.AsLimit

URI: https://scilib.ai/kg/mathlib#Profinite.lim

English

The limit cone X.diagram has a universal cone X.asLimitCone.

Русский

Предел-конус X.diagram имеет универсальный конус X.asLimitCone.

LaTeX

$$$\text{LimitCone}(X.diagram)$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru