asLimitCone'

Mathlib.Topology.Category.Profinite.Extend

URI: https://scilib.ai/kg/mathlib#Profinite.asLimitCone'

Lean4

/-- A cone over `S.diagram'` whose cone point is `S`. -/
abbrev asLimitCone' : Cone (S.diagram') :=
  cone (𝟭 _) S

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

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

Разделы

Аффилиация

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