feat(Topology/Connected): local (path-)connectedness of products and pi types

Mathlib/Topology/Connected/LocallyConnected.lean

@@ -162,4 +162,53 @@ 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
+  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⟩
+
+/-- 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
+  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 ∈ 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

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,56 @@ 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 := fun (x, y) ↦ hasBasis_self.mpr fun U hU ↦ by
+    obtain ⟨u, hu, v, hv, huv⟩ := mem_nhds_prod_iff.mp hU
+    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⟩
+
+/-- 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
+    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 ∈ 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