symm

Mathlib.Topology.Homotopy.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousMap.HomotopicRel.symm

English

If f is Rel-homotopic to g, then g is Rel-homotopic to f (relative to S).

Русский

Если f гомотопно относительно g по S, то g гомотопно относительно f по S.

LaTeX

$$$ \\forall f,g:\\,C(X,Y),\\;HomotopicRel(f,g,S) \\to HomotopicRel(g,f,S)$$$

Lean4

@[symm]
theorem symm ⦃f g : C(X, Y)⦄ (h : HomotopicRel f g S) : HomotopicRel g f S :=
  h.map HomotopyRel.symm

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

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

Разделы

Аффилиация

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