equivalence

Mathlib.Topology.Homotopy.Basic

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

English

For fixed S, the relation f ~_S g defined by HomotopicRel f g S is an equivalence relation.

Русский

Для фиксированного SRelation f \\sim_S g определяется через HomotopicRel как эквивалентность.

LaTeX

$$$ Equivalence\\big(\\lambda f,g:\\,C(X,Y)\\to HomotopicRel(f,g,S)\\big)$$$

Lean4

theorem equivalence : Equivalence fun f g : C(X, Y) => HomotopicRel f g S :=
  ⟨refl, by apply symm, by apply trans⟩

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

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

Разделы

Аффилиация

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