Mathlib v3 is deprecated. Go to Mathlib v4

Theorem unit_interval.Q_right_one_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_right_one_rightView on Github →