pullbackCone_snd_φ

Mathlib.CategoryTheory.Limits.FormalCoproducts

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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