Mathlib Changelog
Changelog
About
Github
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