From ed250f7b7f01c58e473dbe2245de8416c8282278 Mon Sep 17 00:00:00 2001
From: Anatole Dedecker <anatolededecker@gmail.com>
Date: Mon, 20 Dec 2021 20:42:22 +0000
Subject: [PATCH] feat(topology/[path_]connected): add random
 [path-]connectedness lemmas (#10932)

From sphere-eversion
---
 src/topology/connected.lean      | 17 +++++++++++++++++
 src/topology/path_connected.lean |  7 +++++++
 2 files changed, 24 insertions(+)

diff --git a/src/topology/connected.lean b/src/topology/connected.lean
index cad6a6b5be869..d0bac3153f431 100644
--- a/src/topology/connected.lean
+++ b/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 }⟩
diff --git a/src/topology/path_connected.lean b/src/topology/path_connected.lean
index 667f841ce8443..05cd19c7a05b5 100644
--- a/src/topology/path_connected.lean
+++ b/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]