p_fst

Mathlib.AlgebraicTopology.ModelCategory.PathObject

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

English

For a prepath object P over A, the first leg composed with the projection to A×A equals p0: P.p ≫ prod.fst = P.p0.

Русский

Для пред-пути объектa P над A, первая нога после композиции с проекцией в A×A равна p0: P.p ≫ prod.fst = P.p0.

LaTeX

$$$ P.p \;\;\mathrm{comp}\;\; \mathrm{prod.fst} = P.p_0$$$

Lean4

@[reassoc (attr := simp)]
theorem p_fst : P.p ≫ prod.fst = P.p₀ := by simp [p]

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

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

Разделы

Аффилиация

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