instInhabitedUnit

Mathlib.Topology.Homotopy.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousMap.HomotopyEquiv.instInhabitedUnit

English

The symmetry of a transitive composition of homotopy equivalences is the transposed symmetry.

Русский

Симметрия композиции гомотопических эквивалентностей дает симметричную форму.

LaTeX

$$$(h_1\trans h_2).symm = h_2.symm.trans h_1.symm$$$

Lean4

instance : Inhabited (HomotopyEquiv Unit Unit) :=
  ⟨refl Unit⟩

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

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

Разделы

Аффилиация

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