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>

src/topology/connected.lean

@@ -122,18 +122,35 @@ begin
     Hs.is_preconnected Ht.is_preconnected
 end
 
+/-- Theorem of bark and tree :
+if a set is within a (pre)connected set and its closure,
+then it is (pre)connected as well. -/
+theorem is_preconnected.subset_closure {s : set α} {t : set α}
+  (H : is_preconnected s) (Kst : s ⊆ t) (Ktcs : t ⊆ closure s) :
+  is_preconnected t :=
+λ u v hu hv htuv ⟨y, hyt, hyu⟩ ⟨z, hzt, hzv⟩,
+let ⟨p, hpu, hps⟩ := mem_closure_iff.1 (Ktcs hyt) u hu hyu,
+    ⟨q, hqv, hqs⟩ := mem_closure_iff.1 (Ktcs hzt) v hv hzv,
+    ⟨r, hrs, hruv⟩ := H u v hu hv (subset.trans Kst htuv) ⟨p, hps, hpu⟩ ⟨q, hqs, hqv⟩ in
+  ⟨r, Kst hrs, hruv⟩
+
+theorem is_connected.subset_closure {s : set α}  {t : set α}
+  (H : is_connected s) (Kst : s ⊆ t) (Ktcs : t ⊆ closure s): is_connected t :=
+let hsne := H.left,
+    ht := Kst,
+    htne := nonempty.mono ht hsne in
+    ⟨nonempty.mono Kst H.left, is_preconnected.subset_closure H.right Kst Ktcs ⟩
+
+/-- The closure of a (pre)connected set is (pre)connected as well. -/
 theorem is_preconnected.closure {s : set α} (H : is_preconnected s) :
   is_preconnected (closure s) :=
-λ u v hu hv hcsuv ⟨y, hycs, hyu⟩ ⟨z, hzcs, hzv⟩,
-let ⟨p, hpu, hps⟩ := mem_closure_iff.1 hycs u hu hyu in
-let ⟨q, hqv, hqs⟩ := mem_closure_iff.1 hzcs v hv hzv in
-let ⟨r, hrs, hruv⟩ := H u v hu hv (subset.trans subset_closure hcsuv) ⟨p, hps, hpu⟩ ⟨q, hqs, hqv⟩ in
-⟨r, subset_closure hrs, hruv⟩
+is_preconnected.subset_closure H subset_closure $ subset.refl $ closure s
 
 theorem is_connected.closure {s : set α} (H : is_connected s) :
   is_connected (closure s) :=
-⟨H.nonempty.closure, H.is_preconnected.closure⟩
+is_connected.subset_closure H subset_closure $ subset.refl $ closure s
 
+/-- The image of a (pre)connected set is (pre)connected as well. -/
 theorem is_preconnected.image [topological_space β] {s : set α} (H : is_preconnected s)
   (f : α → β) (hf : continuous_on f s) : is_preconnected (f '' s) :=
 begin