leftHomotopyRel — Mathlib

English

From any left homotopy h between f and g, we obtain a relation LeftHomotopyRel f g, i.e., f and g are related by a LeftHomotopy relation.

Русский

Из любой левой гомотопии между f и g получаем отношение LeftHomotopyRel f g, то есть f и g связаны левой гомотопией.

LaTeX

$$$\text{LeftHomotopyRel}(f,g)$$$

Lean4

theorem leftHomotopyRel [CategoryWithWeakEquivalences C] {X Y : C} {f g : X ⟶ Y} {P : Cylinder X}
    (h : P.LeftHomotopy f g) : LeftHomotopyRel f g :=
  ⟨_, ⟨h⟩⟩

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