refl

Mathlib.Topology.Homotopy.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousMap.Homotopic.refl

English

If f is homotopic to g, then g is homotopic to f.

Русский

Если f гомотопно к g, то g гомотопно к f.

LaTeX

$$$$ f \sim g \Rightarrow g \sim f $$$$

Lean4

@[refl]
theorem refl (f : C(X, Y)) : Homotopic f f :=
  ⟨Homotopy.refl f⟩

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

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

Разделы

Аффилиация

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