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