hasWidePullback'

Mathlib.AlgebraicTopology.CechNerve

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CechNerveTerminalFrom.hasWidePullback'

English

An alternative wide pullback exists, often denoted with a prime to indicate a variant construction.

Русский

Существует альтернативный широкий обратный предел, обычно обозначаемый primе.

LaTeX

$$$\\text{HasWidePullback}'(ι, X)$$$

Lean4

instance hasWidePullback' [Finite ι] (X : C) : HasWidePullback (⊤_ C) (fun _ : ι => X) (fun _ => terminal.from X) :=
  hasWidePullback _ _

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

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

Разделы

Аффилиация

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