Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-30 01:12 9208c2bd

View on Github →

feat(topology): path connected spaces

Estimated changes

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 Iic_def

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

added def joined.extend

added theorem joined.extend_one

added theorem joined.extend_zero

added theorem joined.mem_path_component

added theorem joined.refl

added theorem joined.symm

added theorem joined.trans

added def joined

added theorem joined_in.continuous_extend

added theorem joined_in.continuous_map

added def joined_in.extend

added def joined_in.extend_map

added theorem joined_in.extend_map_continuous

added theorem joined_in.extend_map_one

added theorem joined_in.extend_map_zero

added theorem joined_in.extend_one

added theorem joined_in.extend_zero

added theorem joined_in.joined

added def joined_in.map

added theorem joined_in.map_one

added theorem joined_in.map_zero

added theorem joined_in.mem

added theorem joined_in.mono

added theorem joined_in.refl

added theorem joined_in.symm

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 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 theorem path_connected_space.continuous_path

added def path_connected_space.path

added theorem path_connected_space.path_one

added theorem path_connected_space.path_zero

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_subset_basis

added def proj_I

added theorem proj_I_I

added theorem range_proj_I