mathlib3

4d0b3983 - feat(topology/connected): Connectedness of unions of sets (#10005)

feat(topology/connected): Connectedness of unions of sets (#10005) * Add multiple results about when unions of sets are (pre)connected. In particular, the union of connected sets indexed by `ℕ` such that each set intersects the next is connected. * Remove some `set.` prefixes in the file * There are two minor fixes in other files, presumably caused by the fact that they now import `order.succ_pred` * Co-authored by Floris van Doorn fpvdoorn@gmail.com Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr> Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>