mathlib3

fdeb0646 - feat(topology/*): lemmas about `dense`/`dense_range` and `is_(pre)connected` (#8651)

feat(topology/*): lemmas about `dense`/`dense_range` and `is_(pre)connected` (#8651) * add `dense_compl_singleton`; * extract new lemma `is_preconnected_range` from the proof of `is_connected_range`; * add `dense_range.preconnected_space` and `dense_inducing.preconnected_space`; * rename `self_sub_closure_image_preimage_of_open` to `self_subset_closure_image_preimage_of_open`. Inspired by #8579