Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-04 18:21 84b450d4

View on Github →

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

Estimated changes

Modified src/data/set/intervals/basic.lean

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

Modified src/geometry/manifold/real_instances.lean

Modified src/order/filter/bases.lean

added theorem filter.has_basis.to_has_basis

Created src/topology/path_connected.lean

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_open.is_connected_iff_is_path_connected

added theorem is_path_connected.image

added theorem is_path_connected.joined_in

added theorem is_path_connected.mem_path_component

added theorem is_path_connected.preimage_coe

added theorem is_path_connected.subset_path_component

added theorem is_path_connected.union

added def is_path_connected

added theorem is_path_connected_iff

added theorem is_path_connected_iff_eq

added theorem is_path_connected_iff_path_connected_space

added theorem joined.mem_path_component

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.joined_subtype

added theorem joined_in.mem

added theorem joined_in.mono

added theorem joined_in.refl

added def joined_in.some_path

added theorem joined_in.some_path_mem

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 theorem loc_path_connected_of_bases

added theorem loc_path_connected_of_is_open

added theorem mem_path_component_of_mem

added theorem mem_path_component_self

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 theorem path_component.nonempty

added def path_component

added theorem path_component_congr

added def path_component_in

added theorem path_component_in_univ

added theorem path_component_subset_component

added theorem path_component_symm

added def path_connected_space.some_path

added theorem path_connected_space_iff_connected_space

added theorem path_connected_space_iff_eq

added theorem path_connected_space_iff_univ

added theorem path_connected_space_iff_zeroth_homotopy

added theorem path_connected_subset_basis

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