Commit 2020-08-04 18:21 84b450d4

View on Github →

feat(topology): path connected spaces (#3627) From the sphere eversion project.

Estimated changes

added theorem set.Icc_def
added theorem set.Ici_def
added theorem set.Ico_def
added theorem set.Iic_def
added theorem set.Iio_def
added theorem set.Ioc_def
added theorem set.Ioi_def
added theorem set.Ioo_def
added def I_extend
added theorem I_extend_extends
added theorem I_extend_one
added theorem I_extend_range
added theorem I_extend_zero
added def I_symm
added theorem I_symm_one
added theorem I_symm_zero
added theorem Icc_zero_one_symm
added theorem coe_I_one
added theorem coe_I_zero
added theorem continuous.I_extend
added theorem continuous_I_symm
added theorem continuous_proj_I
added theorem is_path_connected_iff
added theorem joined.refl
added def joined.some_path
added theorem joined.symm
added theorem joined.trans
added def joined
added theorem joined_in.joined
added theorem joined_in.mem
added theorem joined_in.mono
added theorem joined_in.refl
added theorem joined_in.source_mem
added theorem joined_in.symm
added theorem joined_in.target_mem
added theorem joined_in.trans
added def joined_in
added theorem joined_in_iff_joined
added theorem joined_in_univ
added def path.cast
added theorem path.cast_coe
added theorem path.continuous_extend
added def path.extend
added theorem path.extend_one
added theorem path.extend_zero
added def path.map
added theorem path.map_coe
added def path.refl
added def path.symm
added def path.trans
added structure path
added def path_component
added theorem path_component_congr
added theorem path_component_in_univ
added theorem path_component_symm
added def path_setoid
added def proj_I
added theorem proj_I_I
added theorem range_proj_I
added theorem surjective_proj_I
added def zeroth_homotopy