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

Created src/data/set/intervals/proj_Icc.lean

added def set.Icc_extend

added theorem set.Icc_extend_coe

added theorem set.Icc_extend_left

added theorem set.Icc_extend_monotone

added theorem set.Icc_extend_of_le_left

added theorem set.Icc_extend_of_mem

added theorem set.Icc_extend_of_right_le

added theorem set.Icc_extend_range

added theorem set.Icc_extend_right

added theorem set.monotone_proj_Icc

added def set.proj_Icc

added theorem set.proj_Icc_coe

added theorem set.proj_Icc_left

added theorem set.proj_Icc_of_le_left

added theorem set.proj_Icc_of_mem

added theorem set.proj_Icc_of_right_le

added theorem set.proj_Icc_right

added theorem set.proj_Icc_surj_on

added theorem set.proj_Icc_surjective

added theorem set.range_proj_Icc

Created src/topology/algebra/ordered/proj_Icc.lean

added theorem continuous.Icc_extend

added theorem continuous_Icc_extend_iff

added theorem continuous_proj_Icc

added theorem quotient_map_proj_Icc

Modified src/topology/basic.lean

added theorem topological_space_eq_iff

Modified src/topology/maps.lean

added theorem quotient_map_iff

Modified src/topology/path_connected.lean

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