one_eq_hSpace_e

Mathlib.Topology.Homotopy.HSpaces

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

English

In a topological group, the unit 1 equals the H-space identity e.

Русский

В топологической группе единица совпадает с единицей H-пространства.

LaTeX

$$$1 = HSpace.e$$$

Lean4

theorem one_eq_hSpace_e {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : (1 : G) = HSpace.e :=
  rfl

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

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

Разделы

Аффилиация

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