feat(topology/[path_]connected): add random [path-]connectedness lemm…

…as (#10932)

From sphere-eversion

src/topology/connected.lean

@@ -518,6 +518,23 @@ begin
     exact ⟨⟨x⟩⟩ }
 end
 
+lemma preconnected_space_iff_connected_component :
+  preconnected_space α ↔ ∀ x : α, connected_component x = univ :=
+begin
+  split,
+  { intros h x,
+    exactI (eq_univ_of_univ_subset $
+      is_preconnected_univ.subset_connected_component (mem_univ x)) },
+  { intros h,
+    casesI is_empty_or_nonempty α with hα hα,
+    { exact ⟨by { rw (univ_eq_empty_iff.mpr hα), exact is_preconnected_empty }⟩ },
+    { exact ⟨by { rw ← h (classical.choice hα), exact is_preconnected_connected_component }⟩ } }
+end
+
+@[simp] lemma preconnected_space.connected_component_eq_univ {X : Type*} [topological_space X]
+  [h : preconnected_space X] (x : X) : connected_component x = univ :=
+preconnected_space_iff_connected_component.mp h x
+
 instance [topological_space β] [preconnected_space α] [preconnected_space β] :
   preconnected_space (α × β) :=
 ⟨by { rw ← univ_prod_univ, exact is_preconnected_univ.prod is_preconnected_univ }⟩

src/topology/path_connected.lean

@@ -884,6 +884,13 @@ begin
   exact (by simpa using hx : path_component x = univ) ▸ path_component_subset_component x
 end
 
+lemma is_path_connected.is_connected (hF : is_path_connected F) : is_connected F :=
+begin
+  rw is_connected_iff_connected_space,
+  rw is_path_connected_iff_path_connected_space at hF,
+  exact @path_connected_space.connected_space _ _ hF
+end
+
 namespace path_connected_space
 variables [path_connected_space X]