asLimit'

Mathlib.Topology.Category.LightProfinite.Extend

URI: https://scilib.ai/kg/mathlib#LightProfinite.asLimit'

Lean4

/-- `S.asLimitCone'` is a limit cone. -/
noncomputable def asLimit' : IsLimit S.asLimitCone' :=
  isLimitCone _ (𝟭 _) S.asLimit S.asLimit

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

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

Разделы

Аффилиация

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