equivalence

Mathlib.Topology.Homotopy.Basic

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

English

The relation of being homotopic is an equivalence relation on the set of continuous maps C(X, Y).

Русский

Отношение гомотопии между отображениями есть эквивалентность на множестве C(X, Y).

LaTeX

$$$$ \text{Homotopic is an equivalence relation on } C(X, Y). $$$$

Lean4

theorem equivalence : Equivalence (@Homotopic X Y _ _) :=
  ⟨refl, by apply symm, by apply trans⟩

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

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

Разделы

Аффилиация

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