mathlib

0ca85a74 - feat(data/set/basic, topology/{subset_properties, connected}): A space is preconnected iff every continuous map to a discrete space is constant (#17070)

feat(data/set/basic, topology/{subset_properties, connected}): A space is preconnected iff every continuous map to a discrete space is constant (#17070) This useful characterisation was missing from mathlib. Co-authored-by: Patrick Massot <patrick.massot@math.cnrs.fr>