chore(Topology): rename pi family from π to X (#26828)

As discussed in [#mathlib4 > Style for naming a pi type in topology/analysis files](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Style.20for.20naming.20a.20pi.20type.20in.20topology.2Fanalysis.20files/with/503532322)

Author: pechersky

Mathlib/Topology/AlexandrovDiscrete.lean

@@ -221,8 +221,8 @@ instance Quotient.instAlexandrovDiscrete {s : Setoid α} : AlexandrovDiscrete (Q
 instance Sum.instAlexandrovDiscrete : AlexandrovDiscrete (α ⊕ β) :=
   alexandrovDiscrete_coinduced.sup alexandrovDiscrete_coinduced
 
-instance Sigma.instAlexandrovDiscrete {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)]
-    [∀ i, AlexandrovDiscrete (π i)] : AlexandrovDiscrete (Σ i, π i) :=
+instance Sigma.instAlexandrovDiscrete {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)]
+    [∀ i, AlexandrovDiscrete (X i)] : AlexandrovDiscrete (Σ i, X i) :=
   alexandrovDiscrete_iSup fun _ ↦ alexandrovDiscrete_coinduced
 
 end

Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean

@@ -303,19 +303,19 @@ end CompleteSpace
 
 section Pi
 
-variable {ι : Type*} {π : α → Type*} [∀ x, CommMonoid (π x)] [∀ x, TopologicalSpace (π x)]
+variable {ι : Type*} {X : α → Type*} [∀ x, CommMonoid (X x)] [∀ x, TopologicalSpace (X x)]
 
 @[to_additive]
-theorem Pi.hasProd {f : ι → ∀ x, π x} {g : ∀ x, π x} :
+theorem Pi.hasProd {f : ι → ∀ x, X x} {g : ∀ x, X x} :
     HasProd f g ↔ ∀ x, HasProd (fun i ↦ f i x) (g x) := by
   simp only [HasProd, tendsto_pi_nhds, prod_apply]
 
 @[to_additive]
-theorem Pi.multipliable {f : ι → ∀ x, π x} : Multipliable f ↔ ∀ x, Multipliable fun i ↦ f i x := by
+theorem Pi.multipliable {f : ι → ∀ x, X x} : Multipliable f ↔ ∀ x, Multipliable fun i ↦ f i x := by
   simp only [Multipliable, Pi.hasProd, Classical.skolem]
 
 @[to_additive]
-theorem tprod_apply [∀ x, T2Space (π x)] {f : ι → ∀ x, π x} {x : α} (hf : Multipliable f) :
+theorem tprod_apply [∀ x, T2Space (X x)] {f : ι → ∀ x, X x} {x : α} (hf : Multipliable f) :
     (∏' i, f i) x = ∏' i, f i x :=
   (Pi.hasProd.mp hf.hasProd x).tprod_eq.symm
 

Mathlib/Topology/Algebra/Module/Equiv.lean

@@ -104,7 +104,7 @@ def iInfKerProjEquiv {I J : Set ι} [DecidablePred fun i => i ∈ I] (hd : Disjo
   toLinearEquiv := LinearMap.iInfKerProjEquiv R φ hd hu
   continuous_toFun :=
     continuous_pi fun i =>
-      Continuous.comp (continuous_apply (π := φ) i) <|
+      Continuous.comp (continuous_apply (A := φ) i) <|
         @continuous_subtype_val _ _ fun x =>
           x ∈ (⨅ i ∈ J, ker (proj i : (∀ i, φ i) →L[R] φ i) : Submodule R (∀ i, φ i))
   continuous_invFun :=

Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

@@ -27,7 +27,7 @@ open scoped Topology
 
 universe u v
 
-variable {ι α β R S : Type*} {π : ι → Type*}
+variable {ι α β R S : Type*} {X : ι → Type*}
 
 section LiminfLimsupAdd
 

Mathlib/Topology/Bases.lean

@@ -576,9 +576,9 @@ theorem isTopologicalBasis_subtype
   h.isInducing ⟨rfl⟩
 
 section
-variable {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)]
+variable {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)]
 
-lemma isOpenMap_eval (i : ι) : IsOpenMap (Function.eval i : (∀ i, π i) → π i) := by
+lemma isOpenMap_eval (i : ι) : IsOpenMap (Function.eval i : (∀ i, X i) → X i) := by
   classical
   refine (isTopologicalBasis_pi fun _ ↦ isTopologicalBasis_opens).isOpenMap_iff.2 ?_
   rintro _ ⟨U, s, hU, rfl⟩
@@ -687,8 +687,8 @@ instance {β} [TopologicalSpace β] [FirstCountableTopology α] [FirstCountableT
 
 section Pi
 
-instance {ι : Type*} {π : ι → Type*} [Countable ι] [∀ i, TopologicalSpace (π i)]
-    [∀ i, FirstCountableTopology (π i)] : FirstCountableTopology (∀ i, π i) :=
+instance {ι : Type*} {X : ι → Type*} [Countable ι] [∀ i, TopologicalSpace (X i)]
+    [∀ i, FirstCountableTopology (X i)] : FirstCountableTopology (∀ i, X i) :=
   ⟨fun f => by rw [nhds_pi]; infer_instance⟩
 
 end Pi
@@ -810,8 +810,8 @@ instance {β : Type*} [TopologicalSpace β] [SecondCountableTopology α] [Second
   ((isBasis_countableBasis α).prod (isBasis_countableBasis β)).secondCountableTopology <|
     (countable_countableBasis α).image2 (countable_countableBasis β) _
 
-instance {ι : Type*} {π : ι → Type*} [Countable ι] [∀ a, TopologicalSpace (π a)]
-    [∀ a, SecondCountableTopology (π a)] : SecondCountableTopology (∀ a, π a) :=
+instance {ι : Type*} {X : ι → Type*} [Countable ι] [∀ a, TopologicalSpace (X a)]
+    [∀ a, SecondCountableTopology (X a)] : SecondCountableTopology (∀ a, X a) :=
   secondCountableTopology_iInf fun _ => secondCountableTopology_induced _ _ _
 
 -- see Note [lower instance priority]
@@ -949,8 +949,8 @@ theorem IsTopologicalBasis.isQuotientMap {V : Set (Set X)} (hV : IsTopologicalBa
     have x_in_W : x ∈ W := y_in_U
     have W_open : IsOpen W := U_open.preimage h'.continuous
     obtain ⟨Z, Z_in_V, x_in_Z, Z_in_W⟩ := hV.exists_subset_of_mem_open x_in_W W_open
-    have πZ_in_U : π '' Z ⊆ U := (Set.image_subset _ Z_in_W).trans (image_preimage_subset π U)
-    exact ⟨π '' Z, ⟨Z, Z_in_V, rfl⟩, ⟨x, x_in_Z, rfl⟩, πZ_in_U⟩
+    have XZ_in_U : π '' Z ⊆ U := (Set.image_subset _ Z_in_W).trans (image_preimage_subset π U)
+    exact ⟨π '' Z, ⟨Z, Z_in_V, rfl⟩, ⟨x, x_in_Z, rfl⟩, XZ_in_U⟩
 
 @[deprecated (since := "2024-10-22")]
 alias IsTopologicalBasis.quotientMap := IsTopologicalBasis.isQuotientMap

Mathlib/Topology/Bornology/Constructions.lean

@@ -9,7 +9,7 @@ import Mathlib.Topology.Bornology.Basic
 /-!
 # Bornology structure on products and subtypes
 
-In this file we define `Bornology` and `BoundedSpace` instances on `α × β`, `Π i, π i`, and
+In this file we define `Bornology` and `BoundedSpace` instances on `α × β`, `Π i, X i`, and
 `{x // p x}`. We also prove basic lemmas about `Bornology.cobounded` and `Bornology.IsBounded`
 on these types.
 -/
@@ -19,16 +19,16 @@ open Set Filter Bornology Function
 
 open Filter
 
-variable {α β ι : Type*} {π : ι → Type*} [Bornology α] [Bornology β]
-  [∀ i, Bornology (π i)]
+variable {α β ι : Type*} {X : ι → Type*} [Bornology α] [Bornology β]
+  [∀ i, Bornology (X i)]
 
 instance Prod.instBornology : Bornology (α × β) where
   cobounded' := (cobounded α).coprod (cobounded β)
   le_cofinite' :=
     @coprod_cofinite α β ▸ coprod_mono ‹Bornology α›.le_cofinite ‹Bornology β›.le_cofinite
 
-instance Pi.instBornology : Bornology (∀ i, π i) where
-  cobounded' := Filter.coprodᵢ fun i => cobounded (π i)
+instance Pi.instBornology : Bornology (∀ i, X i) where
+  cobounded' := Filter.coprodᵢ fun i => cobounded (X i)
   le_cofinite' := iSup_le fun _ ↦ (comap_mono (Bornology.le_cofinite _)).trans (comap_cofinite_le _)
 
 /-- Inverse image of a bornology. -/
@@ -59,7 +59,7 @@ lemma IsBounded.image_fst {s : Set (α × β)} (hs : IsBounded s) : IsBounded (P
 lemma IsBounded.image_snd {s : Set (α × β)} (hs : IsBounded s) : IsBounded (Prod.snd '' s) :=
   (isBounded_image_fst_and_snd.2 hs).2
 
-variable {s : Set α} {t : Set β} {S : ∀ i, Set (π i)}
+variable {s : Set α} {t : Set β} {S : ∀ i, Set (X i)}
 
 theorem IsBounded.fst_of_prod (h : IsBounded (s ×ˢ t)) (ht : t.Nonempty) : IsBounded s :=
   fst_image_prod s ht ▸ h.image_fst
@@ -85,18 +85,18 @@ theorem isBounded_prod_self : IsBounded (s ×ˢ s) ↔ IsBounded s := by
   exact (isBounded_prod_of_nonempty (hs.prod hs)).trans and_self_iff
 
 /-!
-### Bounded sets in `Π i, π i`
+### Bounded sets in `Π i, X i`
 -/
 
 
-theorem cobounded_pi : cobounded (∀ i, π i) = Filter.coprodᵢ fun i => cobounded (π i) :=
+theorem cobounded_pi : cobounded (∀ i, X i) = Filter.coprodᵢ fun i => cobounded (X i) :=
   rfl
 
-theorem forall_isBounded_image_eval_iff {s : Set (∀ i, π i)} :
+theorem forall_isBounded_image_eval_iff {s : Set (∀ i, X i)} :
     (∀ i, IsBounded (eval i '' s)) ↔ IsBounded s :=
   compl_mem_coprodᵢ.symm
 
-lemma IsBounded.image_eval {s : Set (∀ i, π i)} (hs : IsBounded s) (i : ι) :
+lemma IsBounded.image_eval {s : Set (∀ i, X i)} (hs : IsBounded s) (i : ι) :
     IsBounded (eval i '' s) :=
   forall_isBounded_image_eval_iff.2 hs i
 
@@ -139,7 +139,7 @@ open Bornology
 instance [BoundedSpace α] [BoundedSpace β] : BoundedSpace (α × β) := by
   simp [← cobounded_eq_bot_iff, cobounded_prod]
 
-instance [∀ i, BoundedSpace (π i)] : BoundedSpace (∀ i, π i) := by
+instance [∀ i, BoundedSpace (X i)] : BoundedSpace (∀ i, X i) := by
   simp [← cobounded_eq_bot_iff, cobounded_pi]
 
 theorem boundedSpace_induced_iff {α β : Type*} [Bornology β] {f : α → β} :

Mathlib/Topology/Connected/Basic.lean

@@ -38,7 +38,7 @@ open Set Function Topology TopologicalSpace Relation
 
 universe u v
 
-variable {α : Type u} {β : Type v} {ι : Type*} {π : ι → Type*} [TopologicalSpace α]
+variable {α : Type u} {β : Type v} {ι : Type*} {X : ι → Type*} [TopologicalSpace α]
   {s t u v : Set α}
 
 section Preconnected
@@ -423,7 +423,7 @@ theorem IsConnected.prod [TopologicalSpace β] {s : Set α} {t : Set β} (hs : I
     (ht : IsConnected t) : IsConnected (s ×ˢ t) :=
   ⟨hs.1.prod ht.1, hs.2.prod ht.2⟩
 
-theorem isPreconnected_univ_pi [∀ i, TopologicalSpace (π i)] {s : ∀ i, Set (π i)}
+theorem isPreconnected_univ_pi [∀ i, TopologicalSpace (X i)] {s : ∀ i, Set (X i)}
     (hs : ∀ i, IsPreconnected (s i)) : IsPreconnected (pi univ s) := by
   rintro u v uo vo hsuv ⟨f, hfs, hfu⟩ ⟨g, hgs, hgv⟩
   classical
@@ -449,7 +449,7 @@ theorem isPreconnected_univ_pi [∀ i, TopologicalSpace (π i)] {s : ∀ i, Set
     exact inter_subset_inter_left _ hsub
 
 @[simp]
-theorem isConnected_univ_pi [∀ i, TopologicalSpace (π i)] {s : ∀ i, Set (π i)} :
+theorem isConnected_univ_pi [∀ i, TopologicalSpace (X i)] {s : ∀ i, Set (X i)} :
     IsConnected (pi univ s) ↔ ∀ i, IsConnected (s i) := by
   simp only [IsConnected, ← univ_pi_nonempty_iff, forall_and, and_congr_right_iff]
   refine fun hne => ⟨fun hc i => ?_, isPreconnected_univ_pi⟩
@@ -688,11 +688,11 @@ instance [TopologicalSpace β] [PreconnectedSpace α] [PreconnectedSpace β] :
 instance [TopologicalSpace β] [ConnectedSpace α] [ConnectedSpace β] : ConnectedSpace (α × β) :=
   ⟨inferInstance⟩
 
-instance [∀ i, TopologicalSpace (π i)] [∀ i, PreconnectedSpace (π i)] :
-    PreconnectedSpace (∀ i, π i) :=
+instance [∀ i, TopologicalSpace (X i)] [∀ i, PreconnectedSpace (X i)] :
+    PreconnectedSpace (∀ i, X i) :=
   ⟨by rw [← pi_univ univ]; exact isPreconnected_univ_pi fun i => isPreconnected_univ⟩
 
-instance [∀ i, TopologicalSpace (π i)] [∀ i, ConnectedSpace (π i)] : ConnectedSpace (∀ i, π i) :=
+instance [∀ i, TopologicalSpace (X i)] [∀ i, ConnectedSpace (X i)] : ConnectedSpace (∀ i, X i) :=
   ⟨inferInstance⟩
 
 -- see Note [lower instance priority]

Mathlib/Topology/Connected/Clopen.lean

@@ -25,7 +25,7 @@ open Set Function Topology TopologicalSpace Relation
 
 universe u v
 
-variable {α : Type u} {β : Type v} {ι : Type*} {π : ι → Type*} [TopologicalSpace α]
+variable {α : Type u} {β : Type v} {ι : Type*} {X : ι → Type*} [TopologicalSpace α]
   {s t u v : Set α}
 
 section Preconnected
@@ -35,7 +35,7 @@ theorem IsPreconnected.subset_isClopen {s t : Set α} (hs : IsPreconnected s) (h
     (hne : (s ∩ t).Nonempty) : s ⊆ t :=
   hs.subset_left_of_subset_union ht.isOpen ht.compl.isOpen disjoint_compl_right (by simp) hne
 
-theorem Sigma.isConnected_iff [∀ i, TopologicalSpace (π i)] {s : Set (Σ i, π i)} :
+theorem Sigma.isConnected_iff [∀ i, TopologicalSpace (X i)] {s : Set (Σ i, X i)} :
     IsConnected s ↔ ∃ i t, IsConnected t ∧ s = Sigma.mk i '' t := by
   refine ⟨fun hs => ?_, ?_⟩
   · obtain ⟨⟨i, x⟩, hx⟩ := hs.nonempty
@@ -46,8 +46,8 @@ theorem Sigma.isConnected_iff [∀ i, TopologicalSpace (π i)] {s : Set (Σ i, 
   · rintro ⟨i, t, ht, rfl⟩
     exact ht.image _ continuous_sigmaMk.continuousOn
 
-theorem Sigma.isPreconnected_iff [hι : Nonempty ι] [∀ i, TopologicalSpace (π i)]
-    {s : Set (Σ i, π i)} : IsPreconnected s ↔ ∃ i t, IsPreconnected t ∧ s = Sigma.mk i '' t := by
+theorem Sigma.isPreconnected_iff [hι : Nonempty ι] [∀ i, TopologicalSpace (X i)]
+    {s : Set (Σ i, X i)} : IsPreconnected s ↔ ∃ i t, IsPreconnected t ∧ s = Sigma.mk i '' t := by
   refine ⟨fun hs => ?_, ?_⟩
   · obtain rfl | h := s.eq_empty_or_nonempty
     · exact ⟨Classical.choice hι, ∅, isPreconnected_empty, (Set.image_empty _).symm⟩
@@ -88,12 +88,12 @@ theorem Sum.isPreconnected_iff [TopologicalSpace β] {s : Set (α ⊕ β)} :
     · exact ht.image _ continuous_inl.continuousOn
     · exact ht.image _ continuous_inr.continuousOn
 
-/-- A continuous map from a connected space to a disjoint union `Σ i, π i` can be lifted to one of
-the components `π i`. See also `ContinuousMap.exists_lift_sigma` for a version with bundled
+/-- A continuous map from a connected space to a disjoint union `Σ i, X i` can be lifted to one of
+the components `X i`. See also `ContinuousMap.exists_lift_sigma` for a version with bundled
 `ContinuousMap`s. -/
-theorem Continuous.exists_lift_sigma [ConnectedSpace α] [∀ i, TopologicalSpace (π i)]
-    {f : α → Σ i, π i} (hf : Continuous f) :
-    ∃ (i : ι) (g : α → π i), Continuous g ∧ f = Sigma.mk i ∘ g := by
+theorem Continuous.exists_lift_sigma [ConnectedSpace α] [∀ i, TopologicalSpace (X i)]
+    {f : α → Σ i, X i} (hf : Continuous f) :
+    ∃ (i : ι) (g : α → X i), Continuous g ∧ f = Sigma.mk i ∘ g := by
   obtain ⟨i, hi⟩ : ∃ i, range f ⊆ range (.mk i) := by
     rcases Sigma.isConnected_iff.1 (isConnected_range hf) with ⟨i, s, -, hs⟩
     exact ⟨i, hs.trans_subset (image_subset_range _ _)⟩

Mathlib/Topology/Connected/LocallyConnected.lean

@@ -18,7 +18,7 @@ open Set Topology
 
 universe u v
 
-variable {α : Type u} {β : Type v} {ι : Type*} {π : ι → Type*} [TopologicalSpace α]
+variable {α : Type u} {β : Type v} {ι : Type*} {X : ι → Type*} [TopologicalSpace α]
   {s t u v : Set α}
 
 section LocallyConnectedSpace

Mathlib/Topology/Connected/TotallyDisconnected.lean

@@ -22,7 +22,7 @@ open Function Set Topology
 
 universe u v
 
-variable {α : Type u} {β : Type v} {ι : Type*} {π : ι → Type*} [TopologicalSpace α]
+variable {α : Type u} {β : Type v} {ι : Type*} {X : ι → Type*} [TopologicalSpace α]
   {s t u v : Set α}
 
 section TotallyDisconnected
@@ -72,8 +72,8 @@ instance [TopologicalSpace β] [TotallyDisconnectedSpace α] [TotallyDisconnecte
   · exact ht.subsingleton.image _
   · exact ht.subsingleton.image _
 
-instance [∀ i, TopologicalSpace (π i)] [∀ i, TotallyDisconnectedSpace (π i)] :
-    TotallyDisconnectedSpace (Σ i, π i) := by
+instance [∀ i, TopologicalSpace (X i)] [∀ i, TotallyDisconnectedSpace (X i)] :
+    TotallyDisconnectedSpace (Σi, X i) := by
   refine ⟨fun s _ hs => ?_⟩
   obtain rfl | h := s.eq_empty_or_nonempty
   · exact subsingleton_empty