Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-23 19:44 8d33f09c

View on Github →

feat(topology/homotopy/H_spaces): define H spaces (#16029) introduce H-spaces and prove basic properties, in particular that every topological group is a H-space and that the path space at a point is a H-space.

Estimated changes

Modified docs/references.bib

Created src/topology/homotopy/H_spaces.lean

added theorem path.continuous_delay_refl_left

added theorem path.continuous_delay_refl_right

added def path.delay_refl_left

added theorem path.delay_refl_left_one

added theorem path.delay_refl_left_zero

added def path.delay_refl_right

added theorem path.delay_refl_right_one

added theorem path.delay_refl_right_zero

added theorem topological_group.one_eq_H_space_e

added def unit_interval.Q_right

added theorem unit_interval.Q_right_one_left

added theorem unit_interval.Q_right_one_right

added theorem unit_interval.Q_right_zero_left

added theorem unit_interval.Q_right_zero_right

added theorem unit_interval.continuous_Q_right