sndPiMap_π

Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.MulticospanIndex.sndPiMap_π

English

Similarly to fstPiMap, for the second projection Pi.π I.right b, I.sndPiMap ≫ Pi.π I.right b = Pi.π I.left _ ≫ I.snd b.

Русский

Аналогично fstPiMap: I.sndPiMap ≫ Pi.π I.right b = Pi.π I.left _ ≫ I.snd b.

LaTeX

$$$I.sndPiMap \;\circ\; \Pi.π I.right b = \Pi.π I.left (J.snd b) \circ I.snd b$$$

Lean4

@[reassoc (attr := simp)]
theorem sndPiMap_π (b) : I.sndPiMap ≫ Pi.π I.right b = Pi.π I.left _ ≫ I.snd b := by simp [sndPiMap]

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

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

Разделы

Аффилиация

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