Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-13 20:14 fdeb0646

View on Github →

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

Estimated changes

added theorem dense_compl_singleton
added theorem is_preconnected_range