mathlib3

096923c0 - feat(topology/connected.lean): add theorems about connectedness o… (#9633)

feat(topology/connected.lean): add theorems about connectedness o… (#9633) feat(src/topology/connected.lean): add theorems about connectedness of closure add two theorems is_preconnected.inclosure and is_connected.closure which formalize that if a set s is (pre)connected and a set t satisfies s ⊆ t ⊆ closure s, then t is (pre)connected as well modify is_preconnected.closure and is_connected.closure to take these theorems into account add a few comments for theorems in the code Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr> Co-authored-by: Oliver Nash <github@olivernash.org>