Commit 2023-06-02 11:07 c29cd91f

View on Github →

feat: port Topology.Homotopy.HSpaces (#4334)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Homotopy/HSpaces.lean

added theorem Path.continuous_delayReflLeft

added theorem Path.continuous_delayReflRight

added def Path.delayReflLeft

added theorem Path.delayReflLeft_one

added theorem Path.delayReflLeft_zero

added def Path.delayReflRight

added theorem Path.delayReflRight_one

added theorem Path.delayReflRight_zero

added theorem TopologicalGroup.one_eq_hSpace_e

added def TopologicalGroup.toHSpace

added theorem unitInterval.continuous_qRight

added def unitInterval.qRight

added theorem unitInterval.qRight_one_left

added theorem unitInterval.qRight_one_right

added theorem unitInterval.qRight_zero_left

added theorem unitInterval.qRight_zero_right