chore: rename 2 lemmas (#6767)

- `ChartedSpace.locallyCompact` → `ChartedSpace.locallyCompactSpace`
- `ModelWithCorners.locally_compact` → `ModelWithCorners.locallyCompactSpace`

Author: urkud

Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean

@@ -41,8 +41,8 @@ theorem ae_eq_zero_of_integral_smooth_smul_eq_zero (hf : LocallyIntegrable f μ)
     (h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ) g → HasCompactSupport g → ∫ x, g x • f x ∂μ = 0) :
     ∀ᵐ x ∂μ, f x = 0 := by
   -- record topological properties of `M`
-  have := I.locally_compact
-  have := ChartedSpace.locallyCompact H M
+  have := I.locallyCompactSpace
+  have := ChartedSpace.locallyCompactSpace H M
   have := I.secondCountableTopology
   have := ChartedSpace.secondCountable_of_sigma_compact H M
   have := ManifoldWithCorners.metrizableSpace I M

Mathlib/Geometry/Manifold/ChartedSpace.lean

@@ -600,7 +600,7 @@ theorem ChartedSpace.secondCountable_of_sigma_compact [SecondCountableTopology H
 
 /-- If a topological space admits an atlas with locally compact charts, then the space itself
 is locally compact. -/
-theorem ChartedSpace.locallyCompact [LocallyCompactSpace H] : LocallyCompactSpace M := by
+theorem ChartedSpace.locallyCompactSpace [LocallyCompactSpace H] : LocallyCompactSpace M := by
   have : ∀ x : M, (𝓝 x).HasBasis
       (fun s ↦ s ∈ 𝓝 (chartAt H x x) ∧ IsCompact s ∧ s ⊆ (chartAt H x).target)
       fun s ↦ (chartAt H x).symm '' s := fun x ↦ by
@@ -610,7 +610,7 @@ theorem ChartedSpace.locallyCompact [LocallyCompactSpace H] : LocallyCompactSpac
   refine locallyCompactSpace_of_hasBasis this ?_
   rintro x s ⟨_, h₂, h₃⟩
   exact h₂.image_of_continuousOn ((chartAt H x).continuousOn_symm.mono h₃)
-#align charted_space.locally_compact ChartedSpace.locallyCompact
+#align charted_space.locally_compact ChartedSpace.locallyCompactSpace
 
 /-- If a topological space admits an atlas with locally connected charts, then the space itself is
 locally connected. -/

Mathlib/Geometry/Manifold/Metrizable.lean

@@ -25,7 +25,7 @@ theorem ManifoldWithCorners.metrizableSpace {E : Type*} [NormedAddCommGroup E] [
     [FiniteDimensional ℝ E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H)
     (M : Type*) [TopologicalSpace M] [ChartedSpace H M] [SigmaCompactSpace M] [T2Space M] :
     MetrizableSpace M := by
-  haveI := I.locally_compact; haveI := ChartedSpace.locallyCompact H M
+  haveI := I.locallyCompactSpace; haveI := ChartedSpace.locallyCompactSpace H M
   haveI : NormalSpace M := normal_of_paracompact_t2
   haveI := I.secondCountableTopology
   haveI := ChartedSpace.secondCountable_of_sigma_compact H M

Mathlib/Geometry/Manifold/PartitionOfUnity.lean

@@ -341,8 +341,8 @@ theorem exists_isSubordinate [T2Space M] [SigmaCompactSpace M] (hs : IsClosed s)
     (hU : ∀ x ∈ s, U x ∈ 𝓝 x) :
     ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate U := by
   -- First we deduce some missing instances
-  haveI : LocallyCompactSpace H := I.locally_compact
-  haveI : LocallyCompactSpace M := ChartedSpace.locallyCompact H M
+  haveI : LocallyCompactSpace H := I.locallyCompactSpace
+  haveI : LocallyCompactSpace M := ChartedSpace.locallyCompactSpace H M
   haveI : NormalSpace M := normal_of_paracompact_t2
   -- Next we choose a covering by supports of smooth bump functions
   have hB := fun x hx => SmoothBumpFunction.nhds_basis_support I (hU x hx)
@@ -521,8 +521,8 @@ variable [T2Space M] [SigmaCompactSpace M]
 `s`, then there exists a `SmoothPartitionOfUnity ι M s` that is subordinate to `U`. -/
 theorem exists_isSubordinate {s : Set M} (hs : IsClosed s) (U : ι → Set M) (ho : ∀ i, IsOpen (U i))
     (hU : s ⊆ ⋃ i, U i) : ∃ f : SmoothPartitionOfUnity ι I M s, f.IsSubordinate U := by
-  haveI : LocallyCompactSpace H := I.locally_compact
-  haveI : LocallyCompactSpace M := ChartedSpace.locallyCompact H M
+  haveI : LocallyCompactSpace H := I.locallyCompactSpace
+  haveI : LocallyCompactSpace M := ChartedSpace.locallyCompactSpace H M
   haveI : NormalSpace M := normal_of_paracompact_t2
   -- porting note(https://github.com/leanprover/std4/issues/116):
   -- split `rcases` into `have` + `rcases`

Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

@@ -343,7 +343,7 @@ theorem symm_continuousWithinAt_comp_right_iff {X} [TopologicalSpace X] {f : H 
   · rw [← I.left_inv x] at h; exact h.comp I.continuousWithinAt_symm (inter_subset_left _ _)
 #align model_with_corners.symm_continuous_within_at_comp_right_iff ModelWithCorners.symm_continuousWithinAt_comp_right_iff
 
-protected theorem locally_compact [LocallyCompactSpace E] (I : ModelWithCorners 𝕜 E H) :
+protected theorem locallyCompactSpace [LocallyCompactSpace E] (I : ModelWithCorners 𝕜 E H) :
     LocallyCompactSpace H := by
   have : ∀ x : H, (𝓝 x).HasBasis (fun s => s ∈ 𝓝 (I x) ∧ IsCompact s)
       fun s => I.symm '' (s ∩ range I) := fun x ↦ by
@@ -352,7 +352,7 @@ protected theorem locally_compact [LocallyCompactSpace E] (I : ModelWithCorners
   refine' locallyCompactSpace_of_hasBasis this _
   rintro x s ⟨-, hsc⟩
   exact (hsc.inter_right I.closed_range).image I.continuous_symm
-#align model_with_corners.locally_compact ModelWithCorners.locally_compact
+#align model_with_corners.locally_compact ModelWithCorners.locallyCompactSpace
 
 open TopologicalSpace