Mathlib v3 is deprecated. Go to Mathlib v4

Def unit_interval.Q_right

Modification history

2023-05-23 19:44
src/topology/homotopy/H_spaces.lean
feat(topology/homotopy/H_spaces): define H spaces (#16029) …
Added unit_interval.Q_rightView on Github →