Commit 2021-04-08 06:49 8e7028cd

View on Github →

feat(topology/unit_interval): abstract out material about [0,1] (#7056) Separates out some material about [0,1] from topology/path_connected.lean, and adds a very simple tactic.

Estimated changes

Modified src/topology/path_connected.lean

deleted def I_symm

deleted theorem I_symm_one

deleted theorem I_symm_zero

deleted theorem Icc_zero_one_symm

deleted theorem coe_I_one

deleted theorem coe_I_zero

deleted theorem continuous_I_symm

Created src/topology/unit_interval.lean

added theorem unit_interval.coe_one

added theorem unit_interval.coe_zero

added theorem unit_interval.continuous_symm

added theorem unit_interval.le_one

added theorem unit_interval.mem_iff_one_sub_mem

added theorem unit_interval.nonneg

added theorem unit_interval.one_minus_le_one

added theorem unit_interval.one_minus_nonneg

added def unit_interval.symm

added theorem unit_interval.symm_one

added theorem unit_interval.symm_zero

added def unit_interval