Commit 2021-12-24 12:49 6c6c7da8

View on Github →

feat(topology/connected): add inducing.is_preconnected_image (#11011) Generalize the proof of subtype.preconnected_space to any inducing map. Also golf the proof of is_preconnected.subset_right_of_subset_union.

Estimated changes

Modified src/topology/connected.lean

modified theorem continuous.image_connected_component_subset

added theorem continuous.maps_to_connected_component

added theorem inducing.is_preconnected_image

modified theorem preimage_connected_component_connected