chore: rename second_countable -> secondCountable in lemma and instance names (#18911)

While at it, also renames `sigma_compact`, `first_countable` and `locally_compact`, in the same way.

Author: grunweg

Counterexamples/SorgenfreyLine.lean

@@ -324,7 +324,7 @@ theorem not_metrizableSpace : ¬MetrizableSpace ℝₗ := by
 
 /-- Topology on the Sorgenfrey line is not second countable. -/
 theorem not_secondCountableTopology : ¬SecondCountableTopology ℝₗ :=
-  fun _ ↦ not_metrizableSpace (metrizableSpace_of_t3_second_countable _)
+  fun _ ↦ not_metrizableSpace (metrizableSpace_of_t3_secondCountable _)
 
 end SorgenfreyLine
 

Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean

@@ -46,7 +46,7 @@ theorem ae_eq_zero_of_integral_smooth_smul_eq_zero [SigmaCompactSpace M]
   have := I.locallyCompactSpace
   have := ChartedSpace.locallyCompactSpace H M
   have := I.secondCountableTopology
-  have := ChartedSpace.secondCountable_of_sigma_compact H M
+  have := ChartedSpace.secondCountable_of_sigmaCompact H M
   have := Manifold.metrizableSpace I M
   let _ : MetricSpace M := TopologicalSpace.metrizableSpaceMetric M
   -- it suffices to show that the integral of the function vanishes on any compact set `s`
@@ -152,7 +152,7 @@ theorem IsOpen.ae_eq_zero_of_integral_smooth_smul_eq_zero {U : Set M} (hU : IsOp
   haveI := ChartedSpace.locallyCompactSpace H M
   haveI := hU.locallyCompactSpace
   haveI := I.secondCountableTopology
-  haveI := ChartedSpace.secondCountable_of_sigma_compact H M
+  haveI := ChartedSpace.secondCountable_of_sigmaCompact H M
   hU.ae_eq_zero_of_integral_smooth_smul_eq_zero' _
     (isSigmaCompact_iff_sigmaCompactSpace.mpr inferInstance) hf h
 

Mathlib/Analysis/Distribution/SchwartzSpace.lean

@@ -510,7 +510,7 @@ instance instLocallyConvexSpace : LocallyConvexSpace ℝ 𝓢(E, F) :=
   (schwartz_withSeminorms ℝ E F).toLocallyConvexSpace
 
 instance instFirstCountableTopology : FirstCountableTopology 𝓢(E, F) :=
-  (schwartz_withSeminorms ℝ E F).first_countable
+  (schwartz_withSeminorms ℝ E F).firstCountableTopology
 
 end Topology
 

Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

@@ -906,7 +906,7 @@ variable [TopologicalSpace E]
 
 /-- If the topology of a space is induced by a countable family of seminorms, then the topology
 is first countable. -/
-theorem WithSeminorms.first_countable (hp : WithSeminorms p) :
+theorem WithSeminorms.firstCountableTopology (hp : WithSeminorms p) :
     FirstCountableTopology E := by
   have := hp.topologicalAddGroup
   let _ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
@@ -917,4 +917,7 @@ theorem WithSeminorms.first_countable (hp : WithSeminorms p) :
   have : (uniformity E).IsCountablyGenerated := UniformAddGroup.uniformity_countably_generated
   exact UniformSpace.firstCountableTopology E
 
+@[deprecated (since := "2024-11-13")] alias
+WithSeminorms.first_countable := WithSeminorms.firstCountableTopology
+
 end TopologicalProperties

Mathlib/Geometry/Manifold/ChartedSpace.lean

@@ -658,12 +658,15 @@ theorem ChartedSpace.secondCountable_of_countable_cover [SecondCountableTopology
 
 variable (M)
 
-theorem ChartedSpace.secondCountable_of_sigma_compact [SecondCountableTopology H]
+theorem ChartedSpace.secondCountable_of_sigmaCompact [SecondCountableTopology H]
     [SigmaCompactSpace M] : SecondCountableTopology M := by
   obtain ⟨s, hsc, hsU⟩ : ∃ s, Set.Countable s ∧ ⋃ (x) (_ : x ∈ s), (chartAt H x).source = univ :=
-    countable_cover_nhds_of_sigma_compact fun x : M ↦ chart_source_mem_nhds H x
+    countable_cover_nhds_of_sigmaCompact fun x : M ↦ chart_source_mem_nhds H x
   exact ChartedSpace.secondCountable_of_countable_cover H hsU hsc
 
+@[deprecated (since := "2024-11-13")] alias
+ChartedSpace.secondCountable_of_sigma_compact := ChartedSpace.secondCountable_of_sigmaCompact
+
 /-- If a topological space admits an atlas with locally compact charts, then the space itself
 is locally compact. -/
 theorem ChartedSpace.locallyCompactSpace [LocallyCompactSpace H] : LocallyCompactSpace M := by

Mathlib/Geometry/Manifold/Metrizable.lean

@@ -25,7 +25,7 @@ theorem Manifold.metrizableSpace {E : Type*} [NormedAddCommGroup E] [NormedSpace
     MetrizableSpace M := by
   haveI := I.locallyCompactSpace; haveI := ChartedSpace.locallyCompactSpace H M
   haveI := I.secondCountableTopology
-  haveI := ChartedSpace.secondCountable_of_sigma_compact H M
-  exact metrizableSpace_of_t3_second_countable M
+  haveI := ChartedSpace.secondCountable_of_sigmaCompact H M
+  exact metrizableSpace_of_t3_secondCountable M
 @[deprecated (since := "2024-11-11")] alias ManifoldWithCorners.metrizableSpace :=
   Manifold.metrizableSpace

Mathlib/Topology/Algebra/Group/OpenMapping.lean

@@ -46,7 +46,7 @@ theorem smul_singleton_mem_nhds_of_sigmaCompact
   obtain ⟨V, V_mem, V_closed, V_symm, VU⟩ : ∃ V ∈ 𝓝 (1 : G), IsClosed V ∧ V⁻¹ = V ∧ V * V ⊆ U :=
     exists_closed_nhds_one_inv_eq_mul_subset hU
   obtain ⟨s, s_count, hs⟩ : ∃ (s : Set G), s.Countable ∧ ⋃ g ∈ s, g • V = univ :=
-    countable_cover_nhds_of_sigma_compact fun _ ↦ by simpa
+    countable_cover_nhds_of_sigmaCompact fun _ ↦ by simpa
   let K : ℕ → Set G := compactCovering G
   let F : ℕ × s → Set X := fun p ↦ (K p.1 ∩ (p.2 : G) • V) • ({x} : Set X)
   obtain ⟨⟨n, ⟨g, hg⟩⟩, hi⟩ : ∃ i, (interior (F i)).Nonempty := by

Mathlib/Topology/Category/LightProfinite/Basic.lean

@@ -286,7 +286,7 @@ instance {X : LightDiagram} : T2Space ((forget LightDiagram).obj X) :=
 namespace LightProfinite
 
 instance (S : LightProfinite) : Countable (Clopens S) := by
-  rw [TopologicalSpace.Clopens.countable_iff_second_countable]
+  rw [TopologicalSpace.Clopens.countable_iff_secondCountable]
   infer_instance
 
 instance instCountableDiscreteQuotient (S : LightProfinite)  :
@@ -310,7 +310,7 @@ noncomputable def lightProfiniteToLightDiagram : LightProfinite.{u} ⥤ LightDia
 
 open scoped Classical in
 instance (S : LightDiagram.{u}) : SecondCountableTopology S.cone.pt := by
-  rw [← TopologicalSpace.Clopens.countable_iff_second_countable]
+  rw [← TopologicalSpace.Clopens.countable_iff_secondCountable]
   refine @Countable.of_equiv _ _ ?_ (LocallyConstant.equivClopens (X := S.cone.pt))
   refine @Function.Surjective.countable
     (Σ (n : ℕ), LocallyConstant ((S.diagram ⋙ FintypeCat.toProfinite).obj ⟨n⟩) (Fin 2)) _ ?_ ?_ ?_

Mathlib/Topology/ClopenBox.lean

@@ -33,7 +33,9 @@ open scoped Topology
 
 variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace Y]
 
-theorem TopologicalSpace.Clopens.exists_prod_subset (W : Clopens (X × Y)) {a : X × Y} (h : a ∈ W) :
+namespace TopologicalSpace.Clopens
+
+theorem exists_prod_subset (W : Clopens (X × Y)) {a : X × Y} (h : a ∈ W) :
     ∃ U : Clopens X, a.1 ∈ U ∧ ∃ V : Clopens Y, a.2 ∈ V ∧ U ×ˢ V ≤ W := by
   have hp : Continuous (fun y : Y ↦ (a.1, y)) := Continuous.Prod.mk _
   let V : Set Y := {y | (a.1, y) ∈ W}
@@ -47,7 +49,7 @@ variable [CompactSpace X]
 
 /-- Every clopen set in a product of two compact spaces
 is a union of finitely many clopen boxes. -/
-theorem TopologicalSpace.Clopens.exists_finset_eq_sup_prod (W : Clopens (X × Y)) :
+theorem exists_finset_eq_sup_prod (W : Clopens (X × Y)) :
     ∃ (I : Finset (Clopens X × Clopens Y)), W = I.sup fun i ↦ i.1 ×ˢ i.2 := by
   choose! U hxU V hxV hUV using fun x ↦ W.exists_prod_subset (a := x)
   rcases W.2.1.isCompact.elim_nhds_subcover (fun x ↦ U x ×ˢ V x) (fun x hx ↦
@@ -60,21 +62,21 @@ theorem TopologicalSpace.Clopens.exists_finset_eq_sup_prod (W : Clopens (X × Y)
     exact SetLike.le_def.1 (Finset.le_sup hi) hxi
   · exact hUV _ <| hIW _ hx
 
-lemma TopologicalSpace.Clopens.surjective_finset_sup_prod :
+lemma surjective_finset_sup_prod :
     Surjective fun I : Finset (Clopens X × Clopens Y) ↦ I.sup fun i ↦ i.1 ×ˢ i.2 := fun W ↦
   let ⟨I, hI⟩ := W.exists_finset_eq_sup_prod; ⟨I, hI.symm⟩
 
-instance TopologicalSpace.Clopens.countable_prod [Countable (Clopens X)]
+instance countable_prod [Countable (Clopens X)]
     [Countable (Clopens Y)] : Countable (Clopens (X × Y)) :=
   surjective_finset_sup_prod.countable
 
-instance TopologicalSpace.Clopens.finite_prod [Finite (Clopens X)] [Finite (Clopens Y)] :
+instance finite_prod [Finite (Clopens X)] [Finite (Clopens Y)] :
     Finite (Clopens (X × Y)) := by
   cases nonempty_fintype (Clopens X)
   cases nonempty_fintype (Clopens Y)
   exact .of_surjective _ surjective_finset_sup_prod
 
-lemma TopologicalSpace.Clopens.countable_iff_second_countable [T2Space X]
+lemma countable_iff_secondCountable [T2Space X]
     [TotallyDisconnectedSpace X] : Countable (Clopens X) ↔ SecondCountableTopology X := by
   refine ⟨fun h ↦ ⟨{s : Set X | IsClopen s}, ?_, ?_⟩, fun h ↦ ?_⟩
   · let f : {s : Set X | IsClopen s} → Clopens X := fun s ↦ ⟨s.1, s.2⟩
@@ -90,3 +92,8 @@ lemma TopologicalSpace.Clopens.countable_iff_second_countable [T2Space X]
       ext1; change s.carrier = t.carrier
       rw [(this s).choose_spec, (this t).choose_spec, h]
     exact hf.countable
+
+@[deprecated (since := "2024-11-12")]
+alias countable_iff_second_countable := countable_iff_secondCountable
+
+end TopologicalSpace.Clopens

Mathlib/Topology/Compactness/SigmaCompact.lean

@@ -175,21 +175,30 @@ lemma isSigmaCompact_iff_sigmaCompactSpace {s : Set X} :
   isSigmaCompact_iff_isSigmaCompact_univ.trans isSigmaCompact_univ_iff
 
 -- see Note [lower instance priority]
-instance (priority := 200) CompactSpace.sigma_compact [CompactSpace X] : SigmaCompactSpace X :=
+instance (priority := 200) CompactSpace.sigmaCompact [CompactSpace X] : SigmaCompactSpace X :=
   ⟨⟨fun _ => univ, fun _ => isCompact_univ, iUnion_const _⟩⟩
 
+-- The `alias` command creates a definition, triggering the defLemma linter.
+@[nolint defLemma, deprecated (since := "2024-11-13")] alias
+CompactSpace.sigma_compact := CompactSpace.sigmaCompact
+
 theorem SigmaCompactSpace.of_countable (S : Set (Set X)) (Hc : S.Countable)
     (Hcomp : ∀ s ∈ S, IsCompact s) (HU : ⋃₀ S = univ) : SigmaCompactSpace X :=
   ⟨(exists_seq_cover_iff_countable ⟨_, isCompact_empty⟩).2 ⟨S, Hc, Hcomp, HU⟩⟩
 
 -- see Note [lower instance priority]
-instance (priority := 100) sigmaCompactSpace_of_locally_compact_second_countable
+instance (priority := 100) sigmaCompactSpace_of_locallyCompact_secondCountable
     [LocallyCompactSpace X] [SecondCountableTopology X] : SigmaCompactSpace X := by
   choose K hKc hxK using fun x : X => exists_compact_mem_nhds x
   rcases countable_cover_nhds hxK with ⟨s, hsc, hsU⟩
   refine SigmaCompactSpace.of_countable _ (hsc.image K) (forall_mem_image.2 fun x _ => hKc x) ?_
   rwa [sUnion_image]
 
+-- The `alias` command creates a definition, triggering the defLemma linter.
+@[nolint defLemma, deprecated (since := "2024-11-13")]
+alias sigmaCompactSpace_of_locally_compact_second_countable :=
+  sigmaCompactSpace_of_locallyCompact_secondCountable
+
 section
 -- Porting note: doesn't work on the same line
 variable (X)
@@ -289,7 +298,7 @@ protected noncomputable def LocallyFinite.encodable {ι : Type*} {f : ι → Set
 /-- In a topological space with sigma compact topology, if `f` is a function that sends each point
 `x` of a closed set `s` to a neighborhood of `x` within `s`, then for some countable set `t ⊆ s`,
 the neighborhoods `f x`, `x ∈ t`, cover the whole set `s`. -/
-theorem countable_cover_nhdsWithin_of_sigma_compact {f : X → Set X} {s : Set X} (hs : IsClosed s)
+theorem countable_cover_nhdsWithin_of_sigmaCompact {f : X → Set X} {s : Set X} (hs : IsClosed s)
     (hf : ∀ x ∈ s, f x ∈ 𝓝[s] x) : ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x := by
   simp only [nhdsWithin, mem_inf_principal] at hf
   choose t ht hsub using fun n =>
@@ -301,17 +310,22 @@ theorem countable_cover_nhdsWithin_of_sigma_compact {f : X → Set X} {s : Set X
   rcases mem_iUnion₂.1 (hsub n ⟨hn, hx⟩) with ⟨y, hyt : y ∈ t n, hyf : x ∈ s → x ∈ f y⟩
   exact ⟨y, mem_iUnion.2 ⟨n, hyt⟩, hyf hx⟩
 
+@[deprecated (since := "2024-11-13")] alias
+countable_cover_nhdsWithin_of_sigma_compact := countable_cover_nhdsWithin_of_sigmaCompact
+
 /-- In a topological space with sigma compact topology, if `f` is a function that sends each
 point `x` to a neighborhood of `x`, then for some countable set `s`, the neighborhoods `f x`,
 `x ∈ s`, cover the whole space. -/
-theorem countable_cover_nhds_of_sigma_compact {f : X → Set X} (hf : ∀ x, f x ∈ 𝓝 x) :
+theorem countable_cover_nhds_of_sigmaCompact {f : X → Set X} (hf : ∀ x, f x ∈ 𝓝 x) :
     ∃ s : Set X, s.Countable ∧ ⋃ x ∈ s, f x = univ := by
   simp only [← nhdsWithin_univ] at hf
-  rcases countable_cover_nhdsWithin_of_sigma_compact isClosed_univ fun x _ => hf x with
+  rcases countable_cover_nhdsWithin_of_sigmaCompact isClosed_univ fun x _ => hf x with
     ⟨s, -, hsc, hsU⟩
   exact ⟨s, hsc, univ_subset_iff.1 hsU⟩
 end
 
+@[deprecated (since := "2024-11-13")] alias
+countable_cover_nhds_of_sigma_compact := countable_cover_nhds_of_sigmaCompact
 
 
 /-- An [exhaustion by compact sets](https://en.wikipedia.org/wiki/Exhaustion_by_compact_sets) of a