lim'

Mathlib.Topology.Category.LightProfinite.Extend

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

Lean4

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

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

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

Разделы

Аффилиация

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