From a1e38778488353669e8c969653b581e41219b7e7 Mon Sep 17 00:00:00 2001
From: Alex Korbonits <alex@korbonits.com>
Date: Sun, 12 Jul 2026 14:45:04 -0700
Subject: [PATCH] feat(Topology/Connected): connected and path components of
 products and pi types

---
 Mathlib/Topology/Connected/Basic.lean         | 18 +++++++++++
 Mathlib/Topology/Connected/PathConnected.lean | 30 +++++++++++++++++++
 2 files changed, 48 insertions(+)

diff --git a/Mathlib/Topology/Connected/Basic.lean b/Mathlib/Topology/Connected/Basic.lean
index 905b1b9ea09162..f7aba34bab0d86 100644
--- a/Mathlib/Topology/Connected/Basic.lean
+++ b/Mathlib/Topology/Connected/Basic.lean
@@ -627,6 +627,24 @@ theorem Continuous.mapsTo_connectedComponentIn [TopologicalSpace β] {f : α →
     MapsTo f (connectedComponentIn s a) (connectedComponentIn (f '' s) (f a)) :=
   mapsTo_iff_image_subset.2 <| image_connectedComponentIn_subset h hx
 
+/-- The connected component of `(x, y)` in the product space is the product of the connected
+components of `x` and `y`. -/
+theorem connectedComponent_prod [TopologicalSpace β] (x : α) (y : β) :
+    connectedComponent (x, y) = connectedComponent x ×ˢ connectedComponent y :=
+  subset_antisymm
+    (fun _ hp ↦ ⟨continuous_fst.mapsTo_connectedComponent (x, y) hp,
+      continuous_snd.mapsTo_connectedComponent (x, y) hp⟩)
+    (isPreconnected_connectedComponent.prod isPreconnected_connectedComponent
+      |>.subset_connectedComponent ⟨mem_connectedComponent, mem_connectedComponent⟩)
+
+/-- The connected component of `x` in a product space is the product of the connected components
+of its coordinates. -/
+theorem connectedComponent_pi [∀ i, TopologicalSpace (X i)] (x : ∀ i, X i) :
+    connectedComponent x = univ.pi fun i ↦ connectedComponent (x i) :=
+  subset_antisymm (fun _ hy i _ ↦ (continuous_apply i).mapsTo_connectedComponent x hy)
+    (isPreconnected_univ_pi (fun _ ↦ isPreconnected_connectedComponent)
+      |>.subset_connectedComponent fun _ _ ↦ mem_connectedComponent)
+
 theorem irreducibleComponent_subset_connectedComponent {x : α} :
     irreducibleComponent x ⊆ connectedComponent x :=
   isIrreducible_irreducibleComponent.isConnected.subset_connectedComponent mem_irreducibleComponent
diff --git a/Mathlib/Topology/Connected/PathConnected.lean b/Mathlib/Topology/Connected/PathConnected.lean
index b29d16279be30e..7c472c64d2c646 100644
--- a/Mathlib/Topology/Connected/PathConnected.lean
+++ b/Mathlib/Topology/Connected/PathConnected.lean
@@ -78,6 +78,10 @@ theorem Joined.symm {x y : X} (h : Joined x y) : Joined y x :=
 theorem Joined.trans {x y z : X} (hxy : Joined x y) (hyz : Joined y z) : Joined x z :=
   ⟨hxy.somePath.trans hyz.somePath⟩
 
+theorem Joined.map {x y : X} {f : X → Y} (h : Joined x y) (hf : Continuous f) :
+    Joined (f x) (f y) :=
+  ⟨h.somePath.map hf⟩
+
 @[to_additive]
 theorem Joined.mul {M : Type*} [Mul M] [TopologicalSpace M] [ContinuousMul M]
     {a b c d : M} (hs : Joined a b) (ht : Joined c d) : Joined (a * c) (b * d) :=
@@ -607,12 +611,26 @@ section Prod
 
 variable {s : Set X} {t : Set Y}
 
+/-- If `x₁` is joined to `x₂` and `y₁` is joined to `y₂`, then `(x₁, y₁)` is joined to
+`(x₂, y₂)` in the product space. -/
+theorem Joined.prod {x₁ x₂ : X} {y₁ y₂ : Y} (hx : Joined x₁ x₂) (hy : Joined y₁ y₂) :
+    Joined (x₁, y₁) (x₂, y₂) :=
+  ⟨hx.somePath.prod hy.somePath⟩
+
 /-- If `x₁` is joined to `x₂` within `s` and `y₁` to `y₂` within `t`, then `(x₁, y₁)` is joined
 to `(x₂, y₂)` within `s ×ˢ t`. -/
 theorem JoinedIn.prod {x₁ x₂ : X} {y₁ y₂ : Y} (hx : JoinedIn s x₁ x₂) (hy : JoinedIn t y₁ y₂) :
     JoinedIn (s ×ˢ t) (x₁, y₁) (x₂, y₂) :=
   ⟨hx.somePath.prod hy.somePath, by simp⟩
 
+/-- The path component of `(x, y)` in the product space is the product of the path components
+of `x` and `y`. -/
+theorem pathComponent_prod (x : X) (y : Y) :
+    pathComponent (x, y) = pathComponent x ×ˢ pathComponent y := by
+  ext ⟨a, b⟩
+  simp only [Set.mem_prod, mem_pathComponent_iff]
+  exact ⟨fun h ↦ ⟨h.map continuous_fst, h.map continuous_snd⟩, fun ⟨h₁, h₂⟩ ↦ h₁.prod h₂⟩
+
 /-- The product of two path-connected sets is path-connected. -/
 theorem IsPathConnected.prod (hs : IsPathConnected s) (ht : IsPathConnected t) :
     IsPathConnected (s ×ˢ t) := by
@@ -631,12 +649,24 @@ section Pi
 
 variable {Z : ι → Type*} [∀ i, TopologicalSpace (Z i)]
 
+/-- If for each `i`, `x i` is joined to `y i`, then `x` is joined to `y` in the product space. -/
+theorem Joined.pi {x y : ∀ i, Z i} (h : ∀ i, Joined (x i) (y i)) : Joined x y :=
+  ⟨.pi fun i ↦ (h i).somePath⟩
+
 /-- If for each `i`, `x i` is joined to `y i` within `s i`, then `x` is joined to `y` within the
 product set `Set.univ.pi s`. -/
 theorem JoinedIn.pi {s : ∀ i, Set (Z i)} {x y : ∀ i, Z i}
     (h : ∀ i, JoinedIn (s i) (x i) (y i)) : JoinedIn (Set.univ.pi s) x y :=
   ⟨.pi (fun i ↦ (h i).somePath), by simp⟩
 
+/-- The path component of `x` in a product space is the product of the path components of its
+coordinates. -/
+theorem pathComponent_pi (x : ∀ i, Z i) :
+    pathComponent x = Set.univ.pi fun i ↦ pathComponent (x i) := by
+  ext y
+  simp only [Set.mem_univ_pi, mem_pathComponent_iff]
+  exact ⟨fun h i ↦ h.map (continuous_apply i), fun h ↦ .pi h⟩
+
 /-- The product of a family of path-connected sets is path-connected. -/
 theorem IsPathConnected.pi {s : ∀ i, Set (Z i)} (h : ∀ i, IsPathConnected (s i)) :
     IsPathConnected (Set.univ.pi s) := by