hSpace

Mathlib.Topology.Homotopy.HSpaces

URI: https://scilib.ai/kg/mathlib#IsTopologicalGroup.hSpace

English

The H-space structure given by toHSpace G and IsTopologicalGroup.hSpace G are equal.

Русский

Структуры H-пространства из toHSpace G и IsTopologicalGroup.hSpace G равны.

LaTeX

$$$\operatorname{IsTopologicalGroup.hSpace}(G) = \operatorname{IsTopologicalSpace.hSpace}(G)$$$

Lean4

@[to_additive]
instance (priority := 600) hSpace (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : HSpace G :=
  toHSpace G

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

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

Разделы

Аффилиация

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