precomp — Mathlib

English

If f and g are right-homotopic (f ≃_r g), then left-composing with any i: Z → X preserves the right-homotopy relation: i ≫ f and i ≫ g are right-homotopic.

Русский

Если f и g правой гомотопии эквивалентны (f ≃_r g), то левой композицией с любым i: Z → X сохраняется отношение правой гомотопии: i ≫ f и i ≫ g правомотопны.

LaTeX

$$$RightHomotopyRel(f,g) \\Rightarrow \\forall Z, \\forall i: Z \\to X,\\; RightHomotopyRel(i \\circ f, i \\circ g)$$$

Lean4

theorem precomp [CategoryWithWeakEquivalences C] {f g : X ⟶ Y} (h : RightHomotopyRel f g) {Z : C} (i : Z ⟶ X) :
    RightHomotopyRel (i ≫ f) (i ≫ g) := by
  obtain ⟨P, ⟨h⟩⟩ := h
  exact (h.precomp i).rightHomotopyRel

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