ι_sndSigmaMap

Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.MultispanIndex.ι_sndSigmaMap

English

Equality: Sigma.ι I.left b ≫ I.sndSigmaMap = I.snd b ≫ Sigma.ι I.right _.

Русский

Равенство: Sigma.ι I.left b ≫ I.sndSigmaMap = I.snd b ≫ Sigma.ι I.right _.

LaTeX

$$$\Sigma.\ι I.left b \\circ\\ I.sndSigmaMap = I.snd b \\circ\\ \Sigma.\ι I.right _$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_sndSigmaMap (b) : Sigma.ι I.left b ≫ I.sndSigmaMap = I.snd b ≫ Sigma.ι I.right _ := by simp [sndSigmaMap]

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

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

Разделы

Аффилиация

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