mathlib3

6c6c7da8 - feat(topology/connected): add `inducing.is_preconnected_image` (#11011)

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