symm — Mathlib

English

If f and g are right-homotopic, then g and f are right-homotopic as well.

Русский

Если f и g правой гомотопии эквивалентны, то и g и f правой гомотопии эквивалентны.

LaTeX

$$$RightHomotopyRel f g \\Rightarrow RightHomotopyRel g f$$$

Lean4

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

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