12.1. Defining an H-space
Mathlib contains a definition of H-spaces. To say that a type X carries the structure
of an H-space one writes:
variable (H : Type*) [TopologicalSpace H] [HSpace H]
After opening the relevant scope:
open scoped HSpaces
special notation is available for the H-space multiplication:
variable (x y : H)
#check x ⋀ y