p_snd

Mathlib.AlgebraicTopology.ModelCategory.PathObject

URI: https://scilib.ai/kg/mathlib#HomotopicalAlgebra.PrepathObject.p_snd

English

Similarly, P.p composed with the second projection equals p1: P.p ≫ prod.snd = P.p1.

Русский

Аналогично, P.p после композиции с второй проекцией равна p1: P.p ≫ prod.snd = P.p1.

LaTeX

$$$ P.p \;\mathrm{comp}\; \mathrm{prod.snd} = P.p_1$$$

Lean4

@[reassoc (attr := simp)]
theorem p_snd : P.p ≫ prod.snd = P.p₁ := by simp [p]

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

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

Разделы

Аффилиация

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