trans — Mathlib

English

If f0 is right-homotopic to f1 and f1 is right-homotopic to f2, then f0 is right-homotopic to f2.

Русский

Если f0 правой гомотопией эквивалентен f1, а f1 — f2, то f0 правой гомотопии эквивалентен f2.

LaTeX

$$$RightHomotopyRel f_0 f_1 \\rightarrow RightHomotopyRel f_1 f_2 \\rightarrow RightHomotopyRel f_0 f_2$$$

Lean4

theorem trans [ModelCategory C] {f₀ f₁ f₂ : X ⟶ Y} [IsFibrant Y] (h : RightHomotopyRel f₀ f₁)
    (h' : RightHomotopyRel f₁ f₂) : RightHomotopyRel f₀ f₂ :=
  by
  obtain ⟨P, ⟨h⟩⟩ := h
  obtain ⟨P', _, ⟨h'⟩⟩ := h'.exists_good_pathObject
  exact (h.trans h').rightHomotopyRel

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