trans

Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy

URI: https://scilib.ai/kg/mathlib#HomotopicalAlgebra.Precylinder.LeftHomotopy.trans

Lean4

/-- If `f₀` is homotopic to `f₁` relative to a precylinder `P`,
and `f₁` is homotopic to `f₂` relative to `P'`, then
`f₀` is homotopic to `f₂` relative to `P.trans P'`. -/
@[simps]
noncomputable def trans {f₀ f₁ f₂ : X ⟶ Y} (h : P.LeftHomotopy f₀ f₁) {P' : Precylinder X} (h' : P'.LeftHomotopy f₁ f₂)
    [HasPushout P.i₁ P'.i₀] : (P.trans P').LeftHomotopy f₀ f₂ where h := pushout.desc h.h h'.h (by simp)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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