ι_fstSigmaMap

Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

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

English

Equality: Sigma.ι I.left b ≫ I.fstSigmaMap = I.fst b ≫ Sigma.ι I.right _.

Русский

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

LaTeX

$$$\Sigma.\ι I.left b \\circ\\ I.fstSigmaMap = I.fst b \\circ\\ \Sigma.\ι I.right _$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_fstSigmaMap (b) : Sigma.ι I.left b ≫ I.fstSigmaMap = I.fst b ≫ Sigma.ι I.right _ := by simp [fstSigmaMap]

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

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

Разделы

Аффилиация

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