feat(topology/connected): make connected_component_in more usable, …

…develop API (#15964)

From the [Sphere Eversion Project](https://github.com/leanprover-community/sphere-eversion/blob/333231d77aa028bb164abc695ac8a4abce4af0c2/src/to_mathlib/topology/misc.lean#L516)

src/topology/connected.lean

@@ -571,26 +571,85 @@ that contains this point. -/
 def connected_component (x : α) : set α :=
 ⋃₀ { s : set α | is_preconnected s ∧ x ∈ s }
 
-/-- The connected component of a point inside a set. -/
-def connected_component_in (F : set α) (x : F) : set α := coe '' (connected_component x)
+/-- Given a set `F` in a topological space `α` and a point `x : α`, the connected
+component of `x` in `F` is the connected component of `x` in the subtype `F` seen as
+a set in `α`. This definition does not make sense if `x` is not in `F` so we return the
+empty set in this case. -/
+def connected_component_in (F : set α) (x : α) : set α :=
+if h : x ∈ F then coe '' (connected_component (⟨x, h⟩ : F)) else ∅
+
+lemma connected_component_in_eq_image {F : set α} {x : α} (h : x ∈ F) :
+  connected_component_in F x = coe '' (connected_component (⟨x, h⟩ : F)) :=
+dif_pos h
+
+lemma connected_component_in_eq_empty {F : set α} {x : α} (h : x ∉ F) :
+  connected_component_in F x = ∅ :=
+dif_neg h
 
 theorem mem_connected_component {x : α} : x ∈ connected_component x :=
 mem_sUnion_of_mem (mem_singleton x) ⟨is_connected_singleton.is_preconnected, mem_singleton x⟩
 
+theorem mem_connected_component_in {x : α} {F : set α} (hx : x ∈ F) :
+  x ∈ connected_component_in F x :=
+by simp [connected_component_in_eq_image hx, mem_connected_component, hx]
+
+theorem connected_component_nonempty {x : α} :
+  (connected_component x).nonempty :=
+⟨x, mem_connected_component⟩
+
+theorem connected_component_in_nonempty_iff {x : α} {F : set α} :
+  (connected_component_in F x).nonempty ↔ x ∈ F :=
+by { rw [connected_component_in], split_ifs; simp [connected_component_nonempty, h] }
+
+theorem connected_component_in_subset (F : set α) (x : α) :
+  connected_component_in F x ⊆ F :=
+by { rw [connected_component_in], split_ifs; simp }
+
 theorem is_preconnected_connected_component {x : α} : is_preconnected (connected_component x) :=
 is_preconnected_sUnion x _ (λ _, and.right) (λ _, and.left)
 
+lemma is_preconnected_connected_component_in {x : α} {F : set α} :
+  is_preconnected (connected_component_in F x) :=
+begin
+  rw [connected_component_in], split_ifs,
+  { exact embedding_subtype_coe.to_inducing.is_preconnected_image.mpr
+      is_preconnected_connected_component },
+  { exact is_preconnected_empty },
+end
+
 theorem is_connected_connected_component {x : α} : is_connected (connected_component x) :=
 ⟨⟨x, mem_connected_component⟩, is_preconnected_connected_component⟩
 
+lemma is_connected_connected_component_in_iff {x : α} {F : set α} :
+  is_connected (connected_component_in F x) ↔ x ∈ F :=
+by simp_rw [← connected_component_in_nonempty_iff, is_connected,
+  is_preconnected_connected_component_in, and_true]
+
 theorem is_preconnected.subset_connected_component {x : α} {s : set α}
   (H1 : is_preconnected s) (H2 : x ∈ s) : s ⊆ connected_component x :=
 λ z hz, mem_sUnion_of_mem hz ⟨H1, H2⟩
 
+lemma is_preconnected.subset_connected_component_in {x : α} {F : set α} (hs : is_preconnected s)
+  (hxs : x ∈ s) (hsF : s ⊆ F) : s ⊆ connected_component_in F x :=
+begin
+  have : is_preconnected ((coe : F → α) ⁻¹' s),
+  { refine embedding_subtype_coe.to_inducing.is_preconnected_image.mp _,
+    rwa [subtype.image_preimage_coe, inter_eq_left_iff_subset.mpr hsF] },
+  have h2xs : (⟨x, hsF hxs⟩ : F) ∈ coe ⁻¹' s := by { rw [mem_preimage], exact hxs },
+  have := this.subset_connected_component h2xs,
+  rw [connected_component_in_eq_image (hsF hxs)],
+  refine subset.trans _ (image_subset _ this),
+  rw [subtype.image_preimage_coe, inter_eq_left_iff_subset.mpr hsF]
+end
+
 theorem is_connected.subset_connected_component {x : α} {s : set α}
   (H1 : is_connected s) (H2 : x ∈ s) : s ⊆ connected_component x :=
 H1.2.subset_connected_component H2
 
+lemma is_preconnected.connected_component_in {x : α} {F : set α} (h : is_preconnected F)
+  (hx : x ∈ F) : connected_component_in F x = F :=
+(connected_component_in_subset F x).antisymm (h.subset_connected_component_in hx subset_rfl)
+
 theorem connected_component_eq {x y : α} (h : y ∈ connected_component x) :
   connected_component x = connected_component y :=
 eq_of_subset_of_subset
@@ -599,6 +658,23 @@ eq_of_subset_of_subset
     (set.mem_of_mem_of_subset mem_connected_component
       (is_connected_connected_component.subset_connected_component h)))
 
+lemma connected_component_in_eq {x y : α} {F : set α} (h : y ∈ connected_component_in F x) :
+  connected_component_in F x = connected_component_in F y :=
+begin
+  have hx : x ∈ F := connected_component_in_nonempty_iff.mp ⟨y, h⟩,
+  simp_rw [connected_component_in_eq_image hx] at h ⊢,
+  obtain ⟨⟨y, hy⟩, h2y, rfl⟩ := h,
+  simp_rw [subtype.coe_mk, connected_component_in_eq_image hy, connected_component_eq h2y]
+end
+
+theorem connected_component_in_univ (x : α) :
+  connected_component_in univ x = connected_component x :=
+subset_antisymm
+  (is_preconnected_connected_component_in.subset_connected_component $
+    mem_connected_component_in trivial)
+  (is_preconnected_connected_component.subset_connected_component_in mem_connected_component $
+    subset_univ _)
+
 lemma connected_component_disjoint {x y : α} (h : connected_component x ≠ connected_component y) :
   disjoint (connected_component x) (connected_component y) :=
 set.disjoint_left.2 (λ a h1 h2, h
@@ -625,6 +701,18 @@ theorem irreducible_component_subset_connected_component {x : α} :
 is_irreducible_irreducible_component.is_connected.subset_connected_component
   mem_irreducible_component
 
+@[mono]
+lemma connected_component_in_mono (x : α) {F G : set α} (h : F ⊆ G) :
+  connected_component_in F x ⊆ connected_component_in G x :=
+begin
+  by_cases hx : x ∈ F,
+  { rw [connected_component_in_eq_image hx, connected_component_in_eq_image (h hx),
+        ← show (coe : G → α) ∘ inclusion h = coe, by ext ; refl, image_comp],
+    exact image_subset coe ((continuous_inclusion h).image_connected_component_subset ⟨x, hx⟩) },
+  { rw connected_component_in_eq_empty hx,
+    exact set.empty_subset _ },
+end
+
 /-- A preconnected space is one where there is no non-trivial open partition. -/
 class preconnected_space (α : Type u) [topological_space α] : Prop :=
 (is_preconnected_univ : is_preconnected (univ : set α))