Commit 2020-11-27 11:58 8acd296e

View on Github →

chore(topology/path_connected): move proj_Icc to a separate file (#5120) Also use min and max in the definition to make, e.g., the proof of the continuity trivial.

Estimated changes

deleted def I_extend
deleted theorem I_extend_extends
deleted theorem I_extend_one
deleted theorem I_extend_range
deleted theorem I_extend_zero
deleted theorem continuous.I_extend
deleted theorem continuous_proj_I
added theorem path.coe_mk
modified def path.extend
deleted theorem path.extend_le_zero
added theorem path.extend_of_le_zero
added theorem path.extend_of_one_le
deleted theorem path.extend_one_le
deleted def proj_I
deleted theorem proj_I_I
deleted theorem proj_I_one
deleted theorem proj_I_zero
deleted theorem range_proj_I
deleted theorem surjective_proj_I