pullbackCone_snd_f

Mathlib.CategoryTheory.Limits.FormalCoproducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.FormalCoproduct.pullbackCone_snd_f

English

The φ component of the snd projection at i agrees with pb i’s snd component.

Русский

Компонента φ у proj snd на i согласуется с компонентой snd pb i.

LaTeX

$$$(pullbackCone\\ f\\ g\\ pb).snd.\\phi\\ i = (pb\\ i).snd$$$

Lean4

@[simp]
theorem pullbackCone_snd_f (i) : (pullbackCone f g pb).snd.f i = i.1.2 :=
  rfl

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

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

Разделы

Аффилиация

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