Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-30 01:14 4985ad55

View on Github →

Revert "feat(topology): path connected spaces" This reverts commit 9208c2bd1f6c8dedc0cd1646dd107842f05b0b0c.

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 def I_symm
deleted theorem I_symm_one
deleted theorem I_symm_zero
deleted theorem Icc_zero_one_symm
deleted theorem Iic_def
deleted theorem coe_I_one
deleted theorem coe_I_zero
deleted theorem continuous.I_extend
deleted theorem continuous_I_symm
deleted theorem continuous_proj_I
deleted theorem is_path_connected.image
deleted theorem is_path_connected.union
deleted def is_path_connected
deleted theorem is_path_connected_iff
deleted theorem is_path_connected_iff_eq
deleted theorem joined.continuous_extend
deleted def joined.extend
deleted theorem joined.extend_one
deleted theorem joined.extend_zero
deleted theorem joined.mem_path_component
deleted theorem joined.refl
deleted theorem joined.symm
deleted theorem joined.trans
deleted def joined
deleted theorem joined_in.continuous_map
deleted def joined_in.extend
deleted theorem joined_in.extend_map_one
deleted theorem joined_in.extend_map_zero
deleted theorem joined_in.extend_one
deleted theorem joined_in.extend_zero
deleted theorem joined_in.joined
deleted def joined_in.map
deleted theorem joined_in.map_one
deleted theorem joined_in.map_zero
deleted theorem joined_in.mem
deleted theorem joined_in.mono
deleted theorem joined_in.refl
deleted theorem joined_in.symm
deleted theorem joined_in.trans
deleted def joined_in
deleted theorem joined_in_iff_joined
deleted theorem joined_in_univ
deleted theorem mem_path_component_of_mem
deleted theorem mem_path_component_self
deleted theorem path_component.nonempty
deleted def path_component
deleted theorem path_component_congr
deleted def path_component_in
deleted theorem path_component_in_univ
deleted theorem path_component_symm
deleted def proj_I
deleted theorem proj_I_I
deleted theorem range_proj_I