From 4f965970824c9333711d42a3b10e1cbdff79c424 Mon Sep 17 00:00:00 2001
From: Alex Korbonits <alex@korbonits.com>
Date: Sun, 12 Jul 2026 15:01:59 -0700
Subject: [PATCH 1/5] feat(Topology/Connected): products of locally
 (path-)connected spaces are locally (path-)connected

---
 .../Topology/Connected/LocallyConnected.lean  | 46 ++++++++++++++++
 .../Connected/LocallyPathConnected.lean       | 52 +++++++++++++++++++
 2 files changed, 98 insertions(+)

diff --git a/Mathlib/Topology/Connected/LocallyConnected.lean b/Mathlib/Topology/Connected/LocallyConnected.lean
index b634ba83b6634b..840e4bfb57923a 100644
--- a/Mathlib/Topology/Connected/LocallyConnected.lean
+++ b/Mathlib/Topology/Connected/LocallyConnected.lean
@@ -162,4 +162,50 @@ instance [LocallyConnectedSpace α] : DiscreteTopology <| ConnectedComponents α
 instance [LocallyConnectedSpace α] [CompactSpace α] : Finite <| ConnectedComponents α :=
   finite_of_compact_of_discrete
 
+/-- The product of two locally connected spaces is locally connected. -/
+instance Prod.locallyConnectedSpace [TopologicalSpace β] [LocallyConnectedSpace α]
+    [LocallyConnectedSpace β] : LocallyConnectedSpace (α × β) := by
+  rw [locallyConnectedSpace_iff_connected_subsets]
+  rintro ⟨x, y⟩ U hU
+  obtain ⟨u, hu, v, hv, huv⟩ := mem_nhds_prod_iff.mp hU
+  obtain ⟨u', hu', hu'c, hu'u⟩ := locallyConnectedSpace_iff_connected_subsets.mp ‹_› x u hu
+  obtain ⟨v', hv', hv'c, hv'v⟩ := locallyConnectedSpace_iff_connected_subsets.mp ‹_› y v hv
+  exact ⟨u' ×ˢ v', prod_mem_nhds hu' hv', hu'c.prod hv'c, (prod_mono hu'u hv'v).trans huv⟩
+
+/-- A finite product of locally connected spaces is locally connected. -/
+instance Pi.locallyConnectedSpace_of_finite [Finite ι] [∀ i, TopologicalSpace (X i)]
+    [∀ i, LocallyConnectedSpace (X i)] : LocallyConnectedSpace (∀ i, X i) := by
+  rw [locallyConnectedSpace_iff_connected_subsets]
+  intro x U hU
+  rw [nhds_pi, Filter.mem_pi] at hU
+  obtain ⟨I, hI, t, ht, htU⟩ := hU
+  choose V hV hVc hVt using fun i ↦
+    locallyConnectedSpace_iff_connected_subsets.mp inferInstance (x i) (t i) (ht i)
+  exact ⟨univ.pi V, set_pi_mem_nhds finite_univ fun i _ ↦ hV i, isPreconnected_univ_pi hVc,
+    fun f hf ↦ htU fun i hiI ↦ hVt i (hf i trivial)⟩
+
+/-- A product of connected, locally connected spaces is locally connected. Note that an arbitrary
+product of locally connected spaces need not be locally connected, so the connectedness assumption
+cannot be dropped (it can when the index type is finite, see
+`Pi.locallyConnectedSpace_of_finite`). -/
+instance Pi.locallyConnectedSpace [∀ i, TopologicalSpace (X i)]
+    [∀ i, LocallyConnectedSpace (X i)] [∀ i, ConnectedSpace (X i)] :
+    LocallyConnectedSpace (∀ i, X i) := by
+  rw [locallyConnectedSpace_iff_connected_subsets]
+  intro x U hU
+  rw [nhds_pi, Filter.mem_pi] at hU
+  obtain ⟨I, hI, t, ht, htU⟩ := hU
+  choose V hV hVc hVt using fun i ↦
+    locallyConnectedSpace_iff_connected_subsets.mp inferInstance (x i) (t i) (ht i)
+  classical
+  refine ⟨I.pi V, set_pi_mem_nhds hI fun i _ ↦ hV i, ?_,
+    fun f hf ↦ htU fun i hiI ↦ hVt i (hf i hiI)⟩
+  rw [← univ_pi_piecewise_univ]
+  refine isPreconnected_univ_pi fun i ↦ ?_
+  by_cases hi : i ∈ I
+  · rw [piecewise_eq_of_mem _ _ _ hi]
+    exact hVc i
+  · rw [piecewise_eq_of_notMem _ _ _ hi]
+    exact isPreconnected_univ
+
 end LocallyConnectedSpace
diff --git a/Mathlib/Topology/Connected/LocallyPathConnected.lean b/Mathlib/Topology/Connected/LocallyPathConnected.lean
index d26494a7700b2a..fb848812a23e7d 100644
--- a/Mathlib/Topology/Connected/LocallyPathConnected.lean
+++ b/Mathlib/Topology/Connected/LocallyPathConnected.lean
@@ -29,6 +29,9 @@ path-connected, in that each point has a basis of path-connected neighborhoods.
   path-connected spaces are locally path-connected.
 * `Sum.locallyPathConnectedSpace` / `Sigma.locallyPathConnectedSpace`: disjoint unions of locally
   path-connected spaces are locally path-connected.
+* `Prod.locallyPathConnectedSpace` / `Pi.locallyPathConnectedSpace`: binary products of locally
+  path-connected spaces are locally path-connected; likewise for pi types when the index type is
+  finite or all factors are path-connected.
 
 Abstractly, this also shows that locally path-connected spaces form a coreflective subcategory of
 the category of topological spaces, although we do not prove that in this form here.
@@ -299,6 +302,55 @@ instance Sigma.locallyPathConnectedSpace {X : ι → Type*}
 @[deprecated (since := "2026-06-21")]
 alias Sigma.locPathConnectedSpace := Sigma.locallyPathConnectedSpace
 
+/-- The product of two locally path-connected spaces is locally path-connected. -/
+instance Prod.locallyPathConnectedSpace [LocallyPathConnectedSpace Y] :
+    LocallyPathConnectedSpace (X × Y) where
+  path_connected_basis := by
+    rintro ⟨x, y⟩
+    rw [hasBasis_self]
+    intro U hU
+    obtain ⟨u, hu, v, hv, huv⟩ := mem_nhds_prod_iff.mp hU
+    obtain ⟨u', ⟨hu', hu'c⟩, hu'u⟩ := (path_connected_basis x).mem_iff.mp hu
+    obtain ⟨v', ⟨hv', hv'c⟩, hv'v⟩ := (path_connected_basis y).mem_iff.mp hv
+    exact ⟨u' ×ˢ v', prod_mem_nhds hu' hv', hu'c.prod hv'c, (prod_mono hu'u hv'v).trans huv⟩
+
+/-- A finite product of locally path-connected spaces is locally path-connected. -/
+instance Pi.locallyPathConnectedSpace_of_finite [Finite ι] {Z : ι → Type*}
+    [∀ i, TopologicalSpace (Z i)] [∀ i, LocallyPathConnectedSpace (Z i)] :
+    LocallyPathConnectedSpace (∀ i, Z i) where
+  path_connected_basis x := by
+    rw [hasBasis_self]
+    intro U hU
+    rw [nhds_pi, Filter.mem_pi] at hU
+    obtain ⟨J, hJ, t, ht, htU⟩ := hU
+    choose V hV hVt using fun i ↦ (path_connected_basis (x i)).mem_iff.mp (ht i)
+    exact ⟨univ.pi V, set_pi_mem_nhds finite_univ fun i _ ↦ (hV i).1,
+      .pi fun i ↦ (hV i).2, fun f hf ↦ htU fun i hiJ ↦ hVt i (hf i trivial)⟩
+
+/-- A product of path-connected, locally path-connected spaces is locally path-connected. Note
+that an arbitrary product of locally path-connected spaces need not be locally path-connected, so
+the path-connectedness assumption cannot be dropped (it can when the index type is finite, see
+`Pi.locallyPathConnectedSpace_of_finite`). -/
+instance Pi.locallyPathConnectedSpace {Z : ι → Type*} [∀ i, TopologicalSpace (Z i)]
+    [∀ i, LocallyPathConnectedSpace (Z i)] [∀ i, PathConnectedSpace (Z i)] :
+    LocallyPathConnectedSpace (∀ i, Z i) where
+  path_connected_basis x := by
+    rw [hasBasis_self]
+    intro U hU
+    rw [nhds_pi, Filter.mem_pi] at hU
+    obtain ⟨J, hJ, t, ht, htU⟩ := hU
+    choose V hV hVt using fun i ↦ (path_connected_basis (x i)).mem_iff.mp (ht i)
+    classical
+    refine ⟨J.pi V, set_pi_mem_nhds hJ fun i _ ↦ (hV i).1, ?_,
+      fun f hf ↦ htU fun i hiJ ↦ hVt i (hf i hiJ)⟩
+    rw [← univ_pi_piecewise_univ]
+    refine .pi fun i ↦ ?_
+    by_cases hi : i ∈ J
+    · rw [piecewise_eq_of_mem _ _ _ hi]
+      exact (hV i).2
+    · rw [piecewise_eq_of_notMem _ _ _ hi]
+      exact isPathConnected_univ
+
 instance AlexandrovDiscrete.locallyPathConnectedSpace [AlexandrovDiscrete X] :
     LocallyPathConnectedSpace X := by
   apply LocallyPathConnectedSpace.of_bases nhds_basis_nhdsKer_singleton

From 4075c789f4ad593ae9e7c0b26df54ffbd1ade4a4 Mon Sep 17 00:00:00 2001
From: Alex Korbonits <alex@korbonits.com>
Date: Sun, 12 Jul 2026 15:12:49 -0700
Subject: [PATCH 2/5] feat(Topology/Connected): products of locally
 (path-)connected spaces -- edit for concision

---
 .../Topology/Connected/LocallyConnected.lean  | 30 ++++++++--------
 .../Connected/LocallyPathConnected.lean       | 36 +++++++++----------
 2 files changed, 31 insertions(+), 35 deletions(-)

diff --git a/Mathlib/Topology/Connected/LocallyConnected.lean b/Mathlib/Topology/Connected/LocallyConnected.lean
index 840e4bfb57923a..ddefcf1b8c36c8 100644
--- a/Mathlib/Topology/Connected/LocallyConnected.lean
+++ b/Mathlib/Topology/Connected/LocallyConnected.lean
@@ -168,9 +168,10 @@ instance Prod.locallyConnectedSpace [TopologicalSpace β] [LocallyConnectedSpace
   rw [locallyConnectedSpace_iff_connected_subsets]
   rintro ⟨x, y⟩ U hU
   obtain ⟨u, hu, v, hv, huv⟩ := mem_nhds_prod_iff.mp hU
-  obtain ⟨u', hu', hu'c, hu'u⟩ := locallyConnectedSpace_iff_connected_subsets.mp ‹_› x u hu
-  obtain ⟨v', hv', hv'c, hv'v⟩ := locallyConnectedSpace_iff_connected_subsets.mp ‹_› y v hv
-  exact ⟨u' ×ˢ v', prod_mem_nhds hu' hv', hu'c.prod hv'c, (prod_mono hu'u hv'v).trans huv⟩
+  exact ⟨connectedComponentIn u x ×ˢ connectedComponentIn v y,
+    prod_mem_nhds (connectedComponentIn_mem_nhds hu) (connectedComponentIn_mem_nhds hv),
+    isPreconnected_connectedComponentIn.prod isPreconnected_connectedComponentIn,
+    (prod_mono (connectedComponentIn_subset _ _) (connectedComponentIn_subset _ _)).trans huv⟩
 
 /-- A finite product of locally connected spaces is locally connected. -/
 instance Pi.locallyConnectedSpace_of_finite [Finite ι] [∀ i, TopologicalSpace (X i)]
@@ -178,11 +179,11 @@ instance Pi.locallyConnectedSpace_of_finite [Finite ι] [∀ i, TopologicalSpace
   rw [locallyConnectedSpace_iff_connected_subsets]
   intro x U hU
   rw [nhds_pi, Filter.mem_pi] at hU
-  obtain ⟨I, hI, t, ht, htU⟩ := hU
-  choose V hV hVc hVt using fun i ↦
-    locallyConnectedSpace_iff_connected_subsets.mp inferInstance (x i) (t i) (ht i)
-  exact ⟨univ.pi V, set_pi_mem_nhds finite_univ fun i _ ↦ hV i, isPreconnected_univ_pi hVc,
-    fun f hf ↦ htU fun i hiI ↦ hVt i (hf i trivial)⟩
+  obtain ⟨J, hJ, t, ht, htU⟩ := hU
+  exact ⟨univ.pi fun i ↦ connectedComponentIn (t i) (x i),
+    set_pi_mem_nhds finite_univ fun i _ ↦ connectedComponentIn_mem_nhds (ht i),
+    isPreconnected_univ_pi fun i ↦ isPreconnected_connectedComponentIn,
+    fun f hf ↦ htU fun i hiJ ↦ connectedComponentIn_subset _ _ (hf i trivial)⟩
 
 /-- A product of connected, locally connected spaces is locally connected. Note that an arbitrary
 product of locally connected spaces need not be locally connected, so the connectedness assumption
@@ -194,17 +195,16 @@ instance Pi.locallyConnectedSpace [∀ i, TopologicalSpace (X i)]
   rw [locallyConnectedSpace_iff_connected_subsets]
   intro x U hU
   rw [nhds_pi, Filter.mem_pi] at hU
-  obtain ⟨I, hI, t, ht, htU⟩ := hU
-  choose V hV hVc hVt using fun i ↦
-    locallyConnectedSpace_iff_connected_subsets.mp inferInstance (x i) (t i) (ht i)
+  obtain ⟨J, hJ, t, ht, htU⟩ := hU
   classical
-  refine ⟨I.pi V, set_pi_mem_nhds hI fun i _ ↦ hV i, ?_,
-    fun f hf ↦ htU fun i hiI ↦ hVt i (hf i hiI)⟩
+  refine ⟨J.pi fun i ↦ connectedComponentIn (t i) (x i),
+    set_pi_mem_nhds hJ fun i _ ↦ connectedComponentIn_mem_nhds (ht i), ?_,
+    fun f hf ↦ htU fun i hiJ ↦ connectedComponentIn_subset _ _ (hf i hiJ)⟩
   rw [← univ_pi_piecewise_univ]
   refine isPreconnected_univ_pi fun i ↦ ?_
-  by_cases hi : i ∈ I
+  by_cases hi : i ∈ J
   · rw [piecewise_eq_of_mem _ _ _ hi]
-    exact hVc i
+    exact isPreconnected_connectedComponentIn
   · rw [piecewise_eq_of_notMem _ _ _ hi]
     exact isPreconnected_univ
 
diff --git a/Mathlib/Topology/Connected/LocallyPathConnected.lean b/Mathlib/Topology/Connected/LocallyPathConnected.lean
index fb848812a23e7d..86e92b563f5fe5 100644
--- a/Mathlib/Topology/Connected/LocallyPathConnected.lean
+++ b/Mathlib/Topology/Connected/LocallyPathConnected.lean
@@ -305,27 +305,25 @@ alias Sigma.locPathConnectedSpace := Sigma.locallyPathConnectedSpace
 /-- The product of two locally path-connected spaces is locally path-connected. -/
 instance Prod.locallyPathConnectedSpace [LocallyPathConnectedSpace Y] :
     LocallyPathConnectedSpace (X × Y) where
-  path_connected_basis := by
-    rintro ⟨x, y⟩
-    rw [hasBasis_self]
-    intro U hU
+  path_connected_basis := fun (x, y) ↦ hasBasis_self.mpr fun U hU ↦ by
     obtain ⟨u, hu, v, hv, huv⟩ := mem_nhds_prod_iff.mp hU
-    obtain ⟨u', ⟨hu', hu'c⟩, hu'u⟩ := (path_connected_basis x).mem_iff.mp hu
-    obtain ⟨v', ⟨hv', hv'c⟩, hv'v⟩ := (path_connected_basis y).mem_iff.mp hv
-    exact ⟨u' ×ˢ v', prod_mem_nhds hu' hv', hu'c.prod hv'c, (prod_mono hu'u hv'v).trans huv⟩
+    exact ⟨pathComponentIn u x ×ˢ pathComponentIn v y,
+      prod_mem_nhds (pathComponentIn_mem_nhds hu) (pathComponentIn_mem_nhds hv),
+      (isPathConnected_pathComponentIn (mem_of_mem_nhds hu)).prod
+        (isPathConnected_pathComponentIn (mem_of_mem_nhds hv)),
+      (Set.prod_mono pathComponentIn_subset pathComponentIn_subset).trans huv⟩
 
 /-- A finite product of locally path-connected spaces is locally path-connected. -/
 instance Pi.locallyPathConnectedSpace_of_finite [Finite ι] {Z : ι → Type*}
     [∀ i, TopologicalSpace (Z i)] [∀ i, LocallyPathConnectedSpace (Z i)] :
     LocallyPathConnectedSpace (∀ i, Z i) where
-  path_connected_basis x := by
-    rw [hasBasis_self]
-    intro U hU
+  path_connected_basis x := hasBasis_self.mpr fun U hU ↦ by
     rw [nhds_pi, Filter.mem_pi] at hU
     obtain ⟨J, hJ, t, ht, htU⟩ := hU
-    choose V hV hVt using fun i ↦ (path_connected_basis (x i)).mem_iff.mp (ht i)
-    exact ⟨univ.pi V, set_pi_mem_nhds finite_univ fun i _ ↦ (hV i).1,
-      .pi fun i ↦ (hV i).2, fun f hf ↦ htU fun i hiJ ↦ hVt i (hf i trivial)⟩
+    exact ⟨univ.pi fun i ↦ pathComponentIn (t i) (x i),
+      set_pi_mem_nhds finite_univ fun i _ ↦ pathComponentIn_mem_nhds (ht i),
+      .pi fun i ↦ isPathConnected_pathComponentIn (mem_of_mem_nhds (ht i)),
+      fun f hf ↦ htU fun i hiJ ↦ pathComponentIn_subset (hf i trivial)⟩
 
 /-- A product of path-connected, locally path-connected spaces is locally path-connected. Note
 that an arbitrary product of locally path-connected spaces need not be locally path-connected, so
@@ -334,20 +332,18 @@ the path-connectedness assumption cannot be dropped (it can when the index type
 instance Pi.locallyPathConnectedSpace {Z : ι → Type*} [∀ i, TopologicalSpace (Z i)]
     [∀ i, LocallyPathConnectedSpace (Z i)] [∀ i, PathConnectedSpace (Z i)] :
     LocallyPathConnectedSpace (∀ i, Z i) where
-  path_connected_basis x := by
-    rw [hasBasis_self]
-    intro U hU
+  path_connected_basis x := hasBasis_self.mpr fun U hU ↦ by
     rw [nhds_pi, Filter.mem_pi] at hU
     obtain ⟨J, hJ, t, ht, htU⟩ := hU
-    choose V hV hVt using fun i ↦ (path_connected_basis (x i)).mem_iff.mp (ht i)
     classical
-    refine ⟨J.pi V, set_pi_mem_nhds hJ fun i _ ↦ (hV i).1, ?_,
-      fun f hf ↦ htU fun i hiJ ↦ hVt i (hf i hiJ)⟩
+    refine ⟨J.pi fun i ↦ pathComponentIn (t i) (x i),
+      set_pi_mem_nhds hJ fun i _ ↦ pathComponentIn_mem_nhds (ht i), ?_,
+      fun f hf ↦ htU fun i hiJ ↦ pathComponentIn_subset (hf i hiJ)⟩
     rw [← univ_pi_piecewise_univ]
     refine .pi fun i ↦ ?_
     by_cases hi : i ∈ J
     · rw [piecewise_eq_of_mem _ _ _ hi]
-      exact (hV i).2
+      exact isPathConnected_pathComponentIn (mem_of_mem_nhds (ht i))
     · rw [piecewise_eq_of_notMem _ _ _ hi]
       exact isPathConnected_univ
 

From 8db06a86a9cde65575be3d63bfd4ba01fd67a251 Mon Sep 17 00:00:00 2001
From: Alex Korbonits <alex@korbonits.com>
Date: Tue, 14 Jul 2026 23:30:42 -0700
Subject: [PATCH 3/5] responding to @CoolRmal's generous feedback

---
 .../Topology/Connected/LocallyConnected.lean  | 47 +++++++++---------
 .../Connected/LocallyPathConnected.lean       | 49 ++++++++++---------
 2 files changed, 52 insertions(+), 44 deletions(-)

diff --git a/Mathlib/Topology/Connected/LocallyConnected.lean b/Mathlib/Topology/Connected/LocallyConnected.lean
index ddefcf1b8c36c8..8575a255650e85 100644
--- a/Mathlib/Topology/Connected/LocallyConnected.lean
+++ b/Mathlib/Topology/Connected/LocallyConnected.lean
@@ -173,39 +173,42 @@ instance Prod.locallyConnectedSpace [TopologicalSpace β] [LocallyConnectedSpace
     isPreconnected_connectedComponentIn.prod isPreconnected_connectedComponentIn,
     (prod_mono (connectedComponentIn_subset _ _) (connectedComponentIn_subset _ _)).trans huv⟩
 
-/-- A finite product of locally connected spaces is locally connected. -/
-instance Pi.locallyConnectedSpace_of_finite [Finite ι] [∀ i, TopologicalSpace (X i)]
-    [∀ i, LocallyConnectedSpace (X i)] : LocallyConnectedSpace (∀ i, X i) := by
-  rw [locallyConnectedSpace_iff_connected_subsets]
-  intro x U hU
-  rw [nhds_pi, Filter.mem_pi] at hU
-  obtain ⟨J, hJ, t, ht, htU⟩ := hU
-  exact ⟨univ.pi fun i ↦ connectedComponentIn (t i) (x i),
-    set_pi_mem_nhds finite_univ fun i _ ↦ connectedComponentIn_mem_nhds (ht i),
-    isPreconnected_univ_pi fun i ↦ isPreconnected_connectedComponentIn,
-    fun f hf ↦ htU fun i hiJ ↦ connectedComponentIn_subset _ _ (hf i trivial)⟩
-
-/-- A product of connected, locally connected spaces is locally connected. Note that an arbitrary
-product of locally connected spaces need not be locally connected, so the connectedness assumption
-cannot be dropped (it can when the index type is finite, see
-`Pi.locallyConnectedSpace_of_finite`). -/
-instance Pi.locallyConnectedSpace [∀ i, TopologicalSpace (X i)]
-    [∀ i, LocallyConnectedSpace (X i)] [∀ i, ConnectedSpace (X i)] :
+/-- If each `X i` is locally connected and all but finitely many are preconnected, then
+`∀ i, X i` is locally connected. -/
+theorem Pi.locallyConnectedSpace_of_finite_nonpreconnected [∀ i, TopologicalSpace (X i)]
+    [∀ i, LocallyConnectedSpace (X i)] (hfinite : {i | ¬PreconnectedSpace (X i)}.Finite) :
     LocallyConnectedSpace (∀ i, X i) := by
   rw [locallyConnectedSpace_iff_connected_subsets]
   intro x U hU
   rw [nhds_pi, Filter.mem_pi] at hU
   obtain ⟨J, hJ, t, ht, htU⟩ := hU
   classical
-  refine ⟨J.pi fun i ↦ connectedComponentIn (t i) (x i),
-    set_pi_mem_nhds hJ fun i _ ↦ connectedComponentIn_mem_nhds (ht i), ?_,
-    fun f hf ↦ htU fun i hiJ ↦ connectedComponentIn_subset _ _ (hf i hiJ)⟩
+  set K := J ∪ {i | ¬PreconnectedSpace (X i)} with hK
+  refine ⟨K.pi fun i ↦ connectedComponentIn (t i) (x i),
+    set_pi_mem_nhds (hJ.union hfinite) fun i _ ↦ connectedComponentIn_mem_nhds (ht i), ?_,
+    fun f hf ↦ htU fun i hiJ ↦ connectedComponentIn_subset _ _ (hf i (mem_union_left _ hiJ))⟩
   rw [← univ_pi_piecewise_univ]
   refine isPreconnected_univ_pi fun i ↦ ?_
-  by_cases hi : i ∈ J
+  by_cases hi : i ∈ K
   · rw [piecewise_eq_of_mem _ _ _ hi]
     exact isPreconnected_connectedComponentIn
   · rw [piecewise_eq_of_notMem _ _ _ hi]
+    have : PreconnectedSpace (X i) := not_not.mp fun h ↦ hi (hK ▸ mem_union_right _ h)
     exact isPreconnected_univ
 
+/-- A finite product of locally connected spaces is locally connected. -/
+instance Pi.locallyConnectedSpace_of_finite [Finite ι] [∀ i, TopologicalSpace (X i)]
+    [∀ i, LocallyConnectedSpace (X i)] : LocallyConnectedSpace (∀ i, X i) :=
+  locallyConnectedSpace_of_finite_nonpreconnected (Set.toFinite _)
+
+/-- A product of preconnected, locally connected spaces is locally connected. Note that an
+arbitrary product of locally connected spaces need not be locally connected, so the
+preconnectedness assumption cannot be dropped entirely (though it can be dropped for all but
+finitely many factors, see `Pi.locallyConnectedSpace_of_finite_nonpreconnected`). -/
+instance Pi.locallyConnectedSpace [∀ i, TopologicalSpace (X i)]
+    [∀ i, LocallyConnectedSpace (X i)] [∀ i, PreconnectedSpace (X i)] :
+    LocallyConnectedSpace (∀ i, X i) :=
+  locallyConnectedSpace_of_finite_nonpreconnected
+    (Set.finite_empty.subset fun _ hi ↦ (hi inferInstance).elim)
+
 end LocallyConnectedSpace
diff --git a/Mathlib/Topology/Connected/LocallyPathConnected.lean b/Mathlib/Topology/Connected/LocallyPathConnected.lean
index 86e92b563f5fe5..85de973fbf8347 100644
--- a/Mathlib/Topology/Connected/LocallyPathConnected.lean
+++ b/Mathlib/Topology/Connected/LocallyPathConnected.lean
@@ -313,40 +313,45 @@ instance Prod.locallyPathConnectedSpace [LocallyPathConnectedSpace Y] :
         (isPathConnected_pathComponentIn (mem_of_mem_nhds hv)),
       (Set.prod_mono pathComponentIn_subset pathComponentIn_subset).trans huv⟩
 
-/-- A finite product of locally path-connected spaces is locally path-connected. -/
-instance Pi.locallyPathConnectedSpace_of_finite [Finite ι] {Z : ι → Type*}
-    [∀ i, TopologicalSpace (Z i)] [∀ i, LocallyPathConnectedSpace (Z i)] :
-    LocallyPathConnectedSpace (∀ i, Z i) where
-  path_connected_basis x := hasBasis_self.mpr fun U hU ↦ by
-    rw [nhds_pi, Filter.mem_pi] at hU
-    obtain ⟨J, hJ, t, ht, htU⟩ := hU
-    exact ⟨univ.pi fun i ↦ pathComponentIn (t i) (x i),
-      set_pi_mem_nhds finite_univ fun i _ ↦ pathComponentIn_mem_nhds (ht i),
-      .pi fun i ↦ isPathConnected_pathComponentIn (mem_of_mem_nhds (ht i)),
-      fun f hf ↦ htU fun i hiJ ↦ pathComponentIn_subset (hf i trivial)⟩
-
-/-- A product of path-connected, locally path-connected spaces is locally path-connected. Note
-that an arbitrary product of locally path-connected spaces need not be locally path-connected, so
-the path-connectedness assumption cannot be dropped (it can when the index type is finite, see
-`Pi.locallyPathConnectedSpace_of_finite`). -/
-instance Pi.locallyPathConnectedSpace {Z : ι → Type*} [∀ i, TopologicalSpace (Z i)]
-    [∀ i, LocallyPathConnectedSpace (Z i)] [∀ i, PathConnectedSpace (Z i)] :
+/-- If each `Z i` is locally path-connected and all but finitely many are path-connected, then
+`∀ i, Z i` is locally path-connected. -/
+theorem Pi.locallyPathConnectedSpace_of_finite_nonpathconnected {Z : ι → Type*}
+    [∀ i, TopologicalSpace (Z i)] [∀ i, LocallyPathConnectedSpace (Z i)]
+    (hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite) :
     LocallyPathConnectedSpace (∀ i, Z i) where
   path_connected_basis x := hasBasis_self.mpr fun U hU ↦ by
     rw [nhds_pi, Filter.mem_pi] at hU
     obtain ⟨J, hJ, t, ht, htU⟩ := hU
     classical
-    refine ⟨J.pi fun i ↦ pathComponentIn (t i) (x i),
-      set_pi_mem_nhds hJ fun i _ ↦ pathComponentIn_mem_nhds (ht i), ?_,
-      fun f hf ↦ htU fun i hiJ ↦ pathComponentIn_subset (hf i hiJ)⟩
+    set K := J ∪ {i | ¬PathConnectedSpace (Z i)} with hK
+    refine ⟨K.pi fun i ↦ pathComponentIn (t i) (x i),
+      set_pi_mem_nhds (hJ.union hfinite) fun i _ ↦ pathComponentIn_mem_nhds (ht i), ?_,
+      fun f hf ↦ htU fun i hiJ ↦ pathComponentIn_subset (hf i (mem_union_left _ hiJ))⟩
     rw [← univ_pi_piecewise_univ]
     refine .pi fun i ↦ ?_
-    by_cases hi : i ∈ J
+    by_cases hi : i ∈ K
     · rw [piecewise_eq_of_mem _ _ _ hi]
       exact isPathConnected_pathComponentIn (mem_of_mem_nhds (ht i))
     · rw [piecewise_eq_of_notMem _ _ _ hi]
+      have : PathConnectedSpace (Z i) := not_not.mp fun h ↦ hi (hK ▸ mem_union_right _ h)
       exact isPathConnected_univ
 
+/-- A finite product of locally path-connected spaces is locally path-connected. -/
+instance Pi.locallyPathConnectedSpace_of_finite [Finite ι] {Z : ι → Type*}
+    [∀ i, TopologicalSpace (Z i)] [∀ i, LocallyPathConnectedSpace (Z i)] :
+    LocallyPathConnectedSpace (∀ i, Z i) :=
+  locallyPathConnectedSpace_of_finite_nonpathconnected (Set.toFinite _)
+
+/-- A product of path-connected, locally path-connected spaces is locally path-connected. Note
+that an arbitrary product of locally path-connected spaces need not be locally path-connected, so
+the path-connectedness assumption cannot be dropped entirely (though it can be dropped for all but
+finitely many factors, see `Pi.locallyPathConnectedSpace_of_finite_nonpathconnected`). -/
+instance Pi.locallyPathConnectedSpace {Z : ι → Type*} [∀ i, TopologicalSpace (Z i)]
+    [∀ i, LocallyPathConnectedSpace (Z i)] [∀ i, PathConnectedSpace (Z i)] :
+    LocallyPathConnectedSpace (∀ i, Z i) :=
+  locallyPathConnectedSpace_of_finite_nonpathconnected
+    (Set.finite_empty.subset fun _ hi ↦ (hi inferInstance).elim)
+
 instance AlexandrovDiscrete.locallyPathConnectedSpace [AlexandrovDiscrete X] :
     LocallyPathConnectedSpace X := by
   apply LocallyPathConnectedSpace.of_bases nhds_basis_nhdsKer_singleton

From dd50e61cf4839dcf8280d894944c310fa1777abf Mon Sep 17 00:00:00 2001
From: Alex Korbonits <alex@korbonits.com>
Date: Thu, 16 Jul 2026 10:51:08 -0700
Subject: [PATCH 4/5] following up with additional commit per @CoolRmal
 feedback

---
 .../Topology/Connected/LocallyConnected.lean  | 46 +++++++++++++++++++
 .../Connected/LocallyPathConnected.lean       | 33 +++++++++++++
 2 files changed, 79 insertions(+)

diff --git a/Mathlib/Topology/Connected/LocallyConnected.lean b/Mathlib/Topology/Connected/LocallyConnected.lean
index 8575a255650e85..6c1e0effcee270 100644
--- a/Mathlib/Topology/Connected/LocallyConnected.lean
+++ b/Mathlib/Topology/Connected/LocallyConnected.lean
@@ -151,6 +151,22 @@ theorem IsOpen.locallyConnectedSpace [LocallyConnectedSpace α] {U : Set α} (hU
     LocallyConnectedSpace U :=
   hU.isOpenEmbedding_subtypeVal.locallyConnectedSpace
 
+/-- The image of a locally connected space under a quotient map (in particular, under an open
+continuous surjection) is locally connected. -/
+theorem Topology.IsQuotientMap.locallyConnectedSpace [LocallyConnectedSpace α]
+    [TopologicalSpace β] {f : α → β} (hf : IsQuotientMap f) : LocallyConnectedSpace β := by
+  rw [locallyConnectedSpace_iff_connectedComponentIn_open]
+  intro F hF y _
+  rw [← hf.isOpen_preimage, isOpen_iff_mem_nhds]
+  intro x hx
+  have hxF : x ∈ f ⁻¹' F := connectedComponentIn_subset F y hx
+  refine Filter.mem_of_superset
+    ((hF.preimage hf.continuous).connectedComponentIn.mem_nhds (mem_connectedComponentIn hxF))
+    fun z hz ↦ ?_
+  rw [mem_preimage, connectedComponentIn_eq hx]
+  exact connectedComponentIn_mono _ (image_preimage_subset f F)
+    (hf.continuous.mapsTo_connectedComponentIn hxF hz)
+
 /-- If a space is locally connected, the topology of its connected components is discrete. -/
 instance [LocallyConnectedSpace α] : DiscreteTopology <| ConnectedComponents α := by
   refine discreteTopology_iff_isOpen_singleton.mpr fun c ↦ ?_
@@ -211,4 +227,34 @@ instance Pi.locallyConnectedSpace [∀ i, TopologicalSpace (X i)]
   locallyConnectedSpace_of_finite_nonpreconnected
     (Set.finite_empty.subset fun _ hi ↦ (hi inferInstance).elim)
 
+/-- A product of spaces is locally connected iff it is empty, or every factor is locally
+connected and all but finitely many factors are preconnected. -/
+theorem Pi.locallyConnectedSpace_iff [∀ i, TopologicalSpace (X i)] :
+    LocallyConnectedSpace (∀ i, X i) ↔
+      IsEmpty (∀ i, X i) ∨
+        (∀ i, LocallyConnectedSpace (X i)) ∧ {i | ¬PreconnectedSpace (X i)}.Finite := by
+  refine ⟨fun h ↦ ?_, ?_⟩
+  · rcases isEmpty_or_nonempty (∀ i, X i) with he | hne
+    · exact .inl he
+    obtain ⟨x⟩ := hne
+    classical
+    haveI : ∀ i, Nonempty (X i) := Classical.nonempty_pi.mp ⟨x⟩
+    refine .inr ⟨fun i ↦ ((isOpenMap_eval i).isQuotientMap (continuous_apply i)
+      (Function.surjective_eval i)).locallyConnectedSpace, ?_⟩
+    have hVn : connectedComponent x ∈ 𝓝 x :=
+      isOpen_connectedComponent.mem_nhds mem_connectedComponent
+    rw [nhds_pi, Filter.mem_pi] at hVn
+    obtain ⟨J, hJ, t, ht, htV⟩ := hVn
+    refine hJ.subset fun i hi ↦ by_contra fun hiJ ↦ hi ?_
+    suffices himg : Function.eval i '' connectedComponent x = univ by
+      exact ⟨himg ▸ isPreconnected_connectedComponent.image _ (continuous_apply i).continuousOn⟩
+    refine (subset_univ _).antisymm fun z _ ↦
+      ⟨Function.update x i z, htV fun j hj ↦ ?_, by simp⟩
+    rw [Function.update_of_ne (ne_of_mem_of_not_mem hj hiJ)]
+    exact mem_of_mem_nhds (ht j)
+  · rintro (he | ⟨hloc, hfin⟩)
+    · exact ⟨fun x ↦ he.elim x⟩
+    · haveI := hloc
+      exact Pi.locallyConnectedSpace_of_finite_nonpreconnected hfin
+
 end LocallyConnectedSpace
diff --git a/Mathlib/Topology/Connected/LocallyPathConnected.lean b/Mathlib/Topology/Connected/LocallyPathConnected.lean
index 85de973fbf8347..8a2d6e9b46298c 100644
--- a/Mathlib/Topology/Connected/LocallyPathConnected.lean
+++ b/Mathlib/Topology/Connected/LocallyPathConnected.lean
@@ -32,6 +32,9 @@ path-connected, in that each point has a basis of path-connected neighborhoods.
 * `Prod.locallyPathConnectedSpace` / `Pi.locallyPathConnectedSpace`: binary products of locally
   path-connected spaces are locally path-connected; likewise for pi types when the index type is
   finite or all factors are path-connected.
+* `Pi.locallyPathConnectedSpace_iff`: a product of spaces is locally path-connected iff it is
+  empty, or every factor is locally path-connected and all but finitely many factors are
+  path-connected.
 
 Abstractly, this also shows that locally path-connected spaces form a coreflective subcategory of
 the category of topological spaces, although we do not prove that in this form here.
@@ -352,6 +355,36 @@ instance Pi.locallyPathConnectedSpace {Z : ι → Type*} [∀ i, TopologicalSpac
   locallyPathConnectedSpace_of_finite_nonpathconnected
     (Set.finite_empty.subset fun _ hi ↦ (hi inferInstance).elim)
 
+/-- A product of spaces is locally path-connected iff it is empty, or every factor is locally
+path-connected and all but finitely many factors are path-connected. -/
+theorem Pi.locallyPathConnectedSpace_iff {Z : ι → Type*} [∀ i, TopologicalSpace (Z i)] :
+    LocallyPathConnectedSpace (∀ i, Z i) ↔
+      IsEmpty (∀ i, Z i) ∨
+        (∀ i, LocallyPathConnectedSpace (Z i)) ∧ {i | ¬PathConnectedSpace (Z i)}.Finite := by
+  refine ⟨fun h ↦ ?_, ?_⟩
+  · rcases isEmpty_or_nonempty (∀ i, Z i) with he | hne
+    · exact .inl he
+    obtain ⟨x⟩ := hne
+    classical
+    haveI : ∀ i, Nonempty (Z i) := Classical.nonempty_pi.mp ⟨x⟩
+    refine .inr ⟨fun i ↦ ((isOpenMap_eval i).isQuotientMap (continuous_apply i)
+      (surjective_eval i)).locallyPathConnectedSpace, ?_⟩
+    have hVn : pathComponent x ∈ 𝓝 x :=
+      (IsOpen.pathComponent x).mem_nhds (mem_pathComponent_self x)
+    rw [nhds_pi, Filter.mem_pi] at hVn
+    obtain ⟨J, hJ, t, ht, htV⟩ := hVn
+    refine hJ.subset fun i hi ↦ by_contra fun hiJ ↦ hi ?_
+    suffices himg : eval i '' pathComponent x = univ by
+      rw [pathConnectedSpace_iff_univ, ← himg]
+      exact isPathConnected_pathComponent.image (continuous_apply i)
+    refine (subset_univ _).antisymm fun z _ ↦ ⟨update x i z, htV fun j hj ↦ ?_, by simp⟩
+    rw [update_of_ne (ne_of_mem_of_not_mem hj hiJ)]
+    exact mem_of_mem_nhds (ht j)
+  · rintro (he | ⟨hloc, hfin⟩)
+    · exact ⟨fun x ↦ he.elim x⟩
+    · haveI := hloc
+      exact Pi.locallyPathConnectedSpace_of_finite_nonpathconnected hfin
+
 instance AlexandrovDiscrete.locallyPathConnectedSpace [AlexandrovDiscrete X] :
     LocallyPathConnectedSpace X := by
   apply LocallyPathConnectedSpace.of_bases nhds_basis_nhdsKer_singleton

From 3e13aff3655dcab05ef9e7e8be3a970c5a656b45 Mon Sep 17 00:00:00 2001
From: Alex Korbonits <alex@korbonits.com>
Date: Thu, 16 Jul 2026 11:55:02 -0700
Subject: [PATCH 5/5] fixing logical error in docstrings

---
 Mathlib/Topology/Connected/LocallyConnected.lean     | 4 ++--
 Mathlib/Topology/Connected/LocallyPathConnected.lean | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Topology/Connected/LocallyConnected.lean b/Mathlib/Topology/Connected/LocallyConnected.lean
index 6c1e0effcee270..8a2ddd93dba407 100644
--- a/Mathlib/Topology/Connected/LocallyConnected.lean
+++ b/Mathlib/Topology/Connected/LocallyConnected.lean
@@ -219,8 +219,8 @@ instance Pi.locallyConnectedSpace_of_finite [Finite ι] [∀ i, TopologicalSpace
 
 /-- A product of preconnected, locally connected spaces is locally connected. Note that an
 arbitrary product of locally connected spaces need not be locally connected, so the
-preconnectedness assumption cannot be dropped entirely (though it can be dropped for all but
-finitely many factors, see `Pi.locallyConnectedSpace_of_finite_nonpreconnected`). -/
+preconnectedness assumption cannot be dropped entirely (though it can be dropped for finitely
+many factors, see `Pi.locallyConnectedSpace_of_finite_nonpreconnected`). -/
 instance Pi.locallyConnectedSpace [∀ i, TopologicalSpace (X i)]
     [∀ i, LocallyConnectedSpace (X i)] [∀ i, PreconnectedSpace (X i)] :
     LocallyConnectedSpace (∀ i, X i) :=
diff --git a/Mathlib/Topology/Connected/LocallyPathConnected.lean b/Mathlib/Topology/Connected/LocallyPathConnected.lean
index 45b11556f5bb77..2091add763f588 100644
--- a/Mathlib/Topology/Connected/LocallyPathConnected.lean
+++ b/Mathlib/Topology/Connected/LocallyPathConnected.lean
@@ -347,7 +347,7 @@ instance Pi.locallyPathConnectedSpace_of_finite [Finite ι] {Z : ι → Type*}
 
 /-- A product of path-connected, locally path-connected spaces is locally path-connected. Note
 that an arbitrary product of locally path-connected spaces need not be locally path-connected, so
-the path-connectedness assumption cannot be dropped entirely (though it can be dropped for all but
+the path-connectedness assumption cannot be dropped entirely (though it can be dropped for
 finitely many factors, see `Pi.locallyPathConnectedSpace_of_finite_nonpathconnected`). -/
 instance Pi.locallyPathConnectedSpace {Z : ι → Type*} [∀ i, TopologicalSpace (Z i)]
     [∀ i, LocallyPathConnectedSpace (Z i)] [∀ i, PathConnectedSpace (Z i)] :