Commit 2023-10-26 13:37 e43f3621

View on Github →

feat: path-connectedness is preserved by homeomorphisms (#7878) Mirrors the corresponding proofs for connectedness.

Estimated changes

modified theorem Filter.Tendsto.path_extend
added theorem Inseparable.joinedIn
modified theorem IsPathConnected.image'
modified theorem IsPathConnected.image
modified theorem Path.extend_extends'
modified theorem Path.extend_extends
modified theorem Path.extend_of_le_zero
modified theorem Path.extend_of_one_le
modified theorem Path.extend_range
modified def Path.map'
modified def Path.map
modified theorem Path.map_coe
modified theorem Path.map_map
modified theorem Path.map_symm
modified theorem Path.map_trans
modified theorem Path.refl_extend
modified theorem Path.refl_trans_refl
modified theorem Path.symm_cast
modified theorem Path.symm_continuous_family
modified theorem Path.trans_cast
modified theorem Path.trans_range
modified theorem Path.truncate_one_one
modified theorem Path.truncate_range
modified theorem Path.truncate_self
modified theorem Path.truncate_zero_one
modified theorem Path.truncate_zero_zero
added theorem Specializes.joinedIn