12.3. Examples🔗

12.3.1. Topological groups🔗

A topological group G is an H-space. We can witness that Mathlib knows this as follows:

variable (G : Type*) [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G]

IsTopologicalGroup.hSpace G#synth HSpace G

Moreover we can witness that the H-space product is just the group product as follows:

example (g h : G) :
    g * h = g ⋀ h := rfl

12.3.2. Loops🔗

If X is a topological space, Mathlib knows that the space of loops based at a point x is an H-space (in the compact-open topology) with the expected product:

variable (X : Type*) [TopologicalSpace X] (x : X)

Path.instHSpace x#synth HSpace (Path x x)

example (γ γ' : Path x x) :
  γ.trans γ' = γ ⋀ γ' := rfl