chore(Topology/SubsetProperties): rename isCompact_of_isClosed_subset (#7298)

grunweg · grunweg · commit b68cba430a2b · 2023-09-22T11:29:22.000Z
As discussed [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/naming.20in.20docs.23SubsetProperties/near/392310506). Co-authored-by: grunweg <grunweg@posteo.de>
diff --git a/Mathlib/Analysis/Calculus/ContDiffDef.lean b/Mathlib/Analysis/Calculus/ContDiffDef.lean
@@ -1580,7 +1580,7 @@ theorem support_iteratedFDeriv_subset (n : ℕ) : support (iteratedFDeriv 𝕜 n
 
 theorem HasCompactSupport.iteratedFDeriv (hf : HasCompactSupport f) (n : ℕ) :
     HasCompactSupport (iteratedFDeriv 𝕜 n f) :=
-  isCompact_of_isClosed_subset hf isClosed_closure (tsupport_iteratedFDeriv_subset n)
+  hf.of_isClosed_subset isClosed_closure (tsupport_iteratedFDeriv_subset n)
 #align has_compact_support.iterated_fderiv HasCompactSupport.iteratedFDeriv
 
 theorem norm_fderiv_iteratedFDeriv {n : ℕ} :
diff --git a/Mathlib/Analysis/Convex/Exposed.lean b/Mathlib/Analysis/Convex/Exposed.lean
@@ -187,7 +187,7 @@ protected theorem isClosed [OrderClosedTopology 𝕜] {A B : Set E} (hAB : IsExp
 
 protected theorem isCompact [OrderClosedTopology 𝕜] [T2Space E] {A B : Set E}
     (hAB : IsExposed 𝕜 A B) (hA : IsCompact A) : IsCompact B :=
-  isCompact_of_isClosed_subset hA (hAB.isClosed hA.isClosed) hAB.subset
+  hA.of_isClosed_subset (hAB.isClosed hA.isClosed) hAB.subset
 #align is_exposed.is_compact IsExposed.isCompact
 
 end IsExposed
diff --git a/Mathlib/Analysis/Convex/KreinMilman.lean b/Mathlib/Analysis/Convex/KreinMilman.lean
@@ -69,7 +69,7 @@ theorem IsCompact.has_extreme_point (hscomp : IsCompact s) (hsnemp : s.Nonempty)
     by_contra hyx
     obtain ⟨l, hl⟩ := geometric_hahn_banach_point_point hyx
     obtain ⟨z, hzt, hz⟩ :=
-      (isCompact_of_isClosed_subset hscomp htclos hst.1).exists_forall_ge ⟨x, hxt⟩
+      (hscomp.of_isClosed_subset htclos hst.1).exists_forall_ge ⟨x, hxt⟩
         l.continuous.continuousOn
     have h : IsExposed ℝ t ({ z ∈ t | ∀ w ∈ t, l w ≤ l z }) := fun _ => ⟨l, rfl⟩
     rw [← hBmin ({ z ∈ t | ∀ w ∈ t, l w ≤ l z })
@@ -84,7 +84,7 @@ theorem IsCompact.has_extreme_point (hscomp : IsCompact s) (hsnemp : s.Nonempty)
   rw [sInter_eq_iInter]
   refine' IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed _ (fun t u => _)
     (fun t => (hFS t.mem).1)
-    (fun t => isCompact_of_isClosed_subset hscomp (hFS t.mem).2.1 (hFS t.mem).2.2.1) fun t =>
+    (fun t => hscomp.of_isClosed_subset (hFS t.mem).2.1 (hFS t.mem).2.2.1) fun t =>
       (hFS t.mem).2.1
   obtain htu | hut := hF.total t.mem u.mem
   exacts [⟨t, Subset.rfl, htu⟩, ⟨u, hut, Subset.rfl⟩]
diff --git a/Mathlib/Analysis/Convolution.lean b/Mathlib/Analysis/Convolution.lean
@@ -584,7 +584,7 @@ variable [TopologicalAddGroup G]
 
 protected theorem HasCompactSupport.convolution [T2Space G] (hcf : HasCompactSupport f)
     (hcg : HasCompactSupport g) : HasCompactSupport (f ⋆[L, μ] g) :=
-  isCompact_of_isClosed_subset (hcg.isCompact.add hcf) isClosed_closure <|
+  (hcg.isCompact.add hcf).of_isClosed_subset isClosed_closure <|
     closure_minimal
       ((support_convolution_subset_swap L).trans <| add_subset_add subset_closure subset_closure)
       (hcg.isCompact.add hcf).isClosed
@@ -643,7 +643,7 @@ theorem continuousOn_convolution_right_with_param' {g : P → G → E'} {s : Set
     filter_upwards [self_mem_nhdsWithin]
     rintro ⟨p, x⟩ ⟨hp, -⟩
     refine' (HasCompactSupport.convolutionExists_right L _ hf (A _ hp) _).1
-    exact isCompact_of_isClosed_subset hk (isClosed_tsupport _) (B p hp)
+    exact hk.of_isClosed_subset (isClosed_tsupport _) (B p hp)
   let K' := -k + {q₀.2}
   have hK' : IsCompact K' := hk.neg.add isCompact_singleton
   obtain ⟨U, U_open, K'U, hU⟩ : ∃ U, IsOpen U ∧ K' ⊆ U ∧ IntegrableOn f U μ :=
@@ -1270,7 +1270,7 @@ theorem hasFDerivAt_convolution_right_with_param {g : P → G → E'} {s : Set P
     filter_upwards [A' q₀ hq₀]
     rintro ⟨p, x⟩ ⟨hp, -⟩
     refine' (HasCompactSupport.convolutionExists_right L _ hf (A _ hp) _).1
-    apply isCompact_of_isClosed_subset hk (isClosed_tsupport _)
+    apply hk.of_isClosed_subset (isClosed_tsupport _)
     exact closure_minimal (support_subset_iff'.2 fun z hz => hgs _ _ hp hz) hk.isClosed
   have I2 : Integrable (fun a : G => L (f a) (g q₀.1 (q₀.2 - a))) μ := by
     have M : HasCompactSupport (g q₀.1) := HasCompactSupport.intro hk fun x hx => hgs q₀.1 x hq₀ hx
diff --git a/Mathlib/Analysis/NormedSpace/Algebra.lean b/Mathlib/Analysis/NormedSpace/Algebra.lean
@@ -48,7 +48,7 @@ instance [ProperSpace 𝕜] : CompactSpace (characterSpace 𝕜 A) := by
     intro φ hφ
     rw [Set.mem_preimage, mem_closedBall_zero_iff]
     exact (norm_le_norm_one ⟨φ, ⟨hφ.1, hφ.2⟩⟩ : _)
-  exact isCompact_of_isClosed_subset (isCompact_closedBall 𝕜 0 _) CharacterSpace.isClosed h
+  exact (isCompact_closedBall 𝕜 0 _).of_isClosed_subset CharacterSpace.isClosed h
 
 end CharacterSpace
 
diff --git a/Mathlib/Analysis/NormedSpace/FiniteDimension.lean b/Mathlib/Analysis/NormedSpace/FiniteDimension.lean
@@ -488,7 +488,7 @@ theorem HasCompactMulSupport.eq_one_or_finiteDimensional {X : Type*} [Topologica
   obtain ⟨r : ℝ, rpos : 0 < r, hr : Metric.closedBall x r ⊆ Function.mulSupport f⟩ :=
     Metric.nhds_basis_closedBall.mem_iff.1 this
   have : IsCompact (Metric.closedBall x r) :=
-    isCompact_of_isClosed_subset hf Metric.isClosed_ball (hr.trans (subset_mulTSupport _))
+    hf.of_isClosed_subset Metric.isClosed_ball (hr.trans (subset_mulTSupport _))
   exact finiteDimensional_of_isCompact_closedBall 𝕜 rpos this
 #align has_compact_mul_support.eq_one_or_finite_dimensional HasCompactMulSupport.eq_one_or_finiteDimensional
 #align has_compact_support.eq_zero_or_finite_dimensional HasCompactSupport.eq_zero_or_finiteDimensional
@@ -509,14 +509,14 @@ lemma properSpace_of_locallyCompactSpace (𝕜 : Type*) [NontriviallyNormedField
       · simpa [dist_eq_norm, norm_smul, inv_mul_le_iff (pow_pos (zero_lt_one.trans hc) _)] using hy
       · have : c^n ≠ 0 := pow_ne_zero _ (norm_pos_iff.1 (zero_lt_one.trans hc))
         simp [smul_smul, mul_inv_cancel this]
-    exact isCompact_of_isClosed_subset (hr.image Cf) isClosed_ball A
+    exact (hr.image Cf).of_isClosed_subset isClosed_ball A
   refine ⟨fun x s ↦ ?_⟩
   have L : ∀ᶠ n in (atTop : Filter ℕ), s ≤ ‖c‖^n * r := by
     have : Tendsto (fun n ↦ ‖c‖^n * r) atTop atTop :=
       Tendsto.atTop_mul_const rpos (tendsto_pow_atTop_atTop_of_one_lt hc)
     exact Tendsto.eventually_ge_atTop this s
   rcases L.exists with ⟨n, hn⟩
-  exact isCompact_of_isClosed_subset (M n x) isClosed_ball (closedBall_subset_closedBall hn)
+  exact (M n x).of_isClosed_subset isClosed_ball (closedBall_subset_closedBall hn)
 
 end Riesz
 
@@ -620,7 +620,7 @@ nonrec theorem IsCompact.exists_mem_frontier_infDist_compl_eq_dist {E : Type*}
     rcases hx' with ⟨r, hr₀, hrK⟩
     have : FiniteDimensional ℝ E :=
       finiteDimensional_of_isCompact_closedBall ℝ hr₀
-        (isCompact_of_isClosed_subset hK Metric.isClosed_ball hrK)
+        (hK.of_isClosed_subset Metric.isClosed_ball hrK)
     exact exists_mem_frontier_infDist_compl_eq_dist hx hK.ne_univ
   · refine' ⟨x, hx', _⟩
     rw [frontier_eq_closure_inter_closure] at hx'
diff --git a/Mathlib/Dynamics/OmegaLimit.lean b/Mathlib/Dynamics/OmegaLimit.lean
@@ -237,7 +237,7 @@ theorem eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit
   rcases hc₂ with ⟨v, hv₁, hv₂⟩
   let k := closure (image2 ϕ v s)
   have hk : IsCompact (k \ n) :=
-    IsCompact.diff (isCompact_of_isClosed_subset hc₁ isClosed_closure hv₂) hn₁
+    (hc₁.of_isClosed_subset isClosed_closure hv₂).diff hn₁
   let j u := (closure (image2 ϕ (u ∩ v) s))ᶜ
   have hj₁ : ∀ u ∈ f, IsOpen (j u) := fun _ _ ↦ isOpen_compl_iff.mpr isClosed_closure
   have hj₂ : k \ n ⊆ ⋃ u ∈ f, j u := by
@@ -315,7 +315,7 @@ theorem nonempty_omegaLimit_of_isCompact_absorbing [NeBot f] {c : Set β} (hc₁
       Nonempty.image2 (Filter.nonempty_of_mem (inter_mem u.prop hv₁)) hs
     exact hn.mono subset_closure
   · intro
-    apply isCompact_of_isClosed_subset hc₁ isClosed_closure
+    apply hc₁.of_isClosed_subset isClosed_closure
     calc
       _ ⊆ closure (image2 ϕ v s) := closure_mono (image2_subset (inter_subset_right _ _) Subset.rfl)
       _ ⊆ c := hv₂
diff --git a/Mathlib/Geometry/Manifold/BumpFunction.lean b/Mathlib/Geometry/Manifold/BumpFunction.lean
@@ -277,7 +277,7 @@ theorem tsupport_subset_chartAt_source : tsupport f ⊆ (chartAt H c).source :=
 #align smooth_bump_function.tsupport_subset_chart_at_source SmoothBumpFunction.tsupport_subset_chartAt_source
 
 protected theorem hasCompactSupport : HasCompactSupport f :=
-  isCompact_of_isClosed_subset f.isCompact_symm_image_closedBall isClosed_closure
+  f.isCompact_symm_image_closedBall.of_isClosed_subset isClosed_closure
     f.tsupport_subset_symm_image_closedBall
 #align smooth_bump_function.has_compact_support SmoothBumpFunction.hasCompactSupport
 
diff --git a/Mathlib/MeasureTheory/Function/LocallyIntegrable.lean b/Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
@@ -144,7 +144,7 @@ theorem locallyIntegrableOn_iff [LocallyCompactSpace X] [T2Space X] (hs : IsClos
       let ⟨K, hK, h2K⟩ := exists_compact_mem_nhds x
       ⟨_, inter_mem_nhdsWithin s h2K,
         hf _ (inter_subset_left _ _)
-          (isCompact_of_isClosed_subset hK (hs.inter hK.isClosed) (inter_subset_right _ _))⟩
+          (hK.of_isClosed_subset (hs.inter hK.isClosed) (inter_subset_right _ _))⟩
   | inr hs =>
     obtain ⟨K, hK, h2K, h3K⟩ := exists_compact_subset hs hx
     refine' ⟨K, _, hf K h3K hK⟩
diff --git a/Mathlib/Topology/Algebra/Group/Basic.lean b/Mathlib/Topology/Algebra/Group/Basic.lean
@@ -1715,7 +1715,7 @@ theorem exists_isCompact_isClosed_subset_isCompact_nhds_one
         mul_subset_mul_right <| singleton_subset_iff.2 hV₁
       _ = V * V := hVo.mul_closure _
       _ ⊆ L := hVL
-  exact ⟨closure V, isCompact_of_isClosed_subset Lcomp isClosed_closure hcVL, isClosed_closure,
+  exact ⟨closure V, Lcomp.of_isClosed_subset isClosed_closure hcVL, isClosed_closure,
     hcVL, mem_of_superset (hVo.mem_nhds hV₁) subset_closure⟩
 
 /-- In a locally compact group, any neighborhood of the identity contains a compact closed
diff --git a/Mathlib/Topology/Compactification/OnePoint.lean b/Mathlib/Topology/Compactification/OnePoint.lean
@@ -196,7 +196,7 @@ instance : TopologicalSpace (OnePoint X) where
     suffices IsOpen ((↑) ⁻¹' ⋃₀ S : Set X) by
       refine' ⟨_, this⟩
       rintro ⟨s, hsS : s ∈ S, hs : ∞ ∈ s⟩
-      refine' isCompact_of_isClosed_subset ((ho s hsS).1 hs) this.isClosed_compl _
+      refine' IsCompact.of_isClosed_subset ((ho s hsS).1 hs) this.isClosed_compl _
       exact compl_subset_compl.mpr (preimage_mono <| subset_sUnion_of_mem hsS)
     rw [preimage_sUnion]
     exact isOpen_biUnion fun s hs => (ho s hs).2
diff --git a/Mathlib/Topology/ContinuousFunction/Bounded.lean b/Mathlib/Topology/ContinuousFunction/Bounded.lean
@@ -587,7 +587,7 @@ theorem arzela_ascoli₂ (s : Set β) (hs : IsCompact s) (A : Set (α →ᵇ β)
   using compactness there and then lifting everything to the original space. -/
   have M : LipschitzWith 1 (↑) := LipschitzWith.subtype_val s
   let F : (α →ᵇ s) → α →ᵇ β := comp (↑) M
-  refine' isCompact_of_isClosed_subset ((_ : IsCompact (F ⁻¹' A)).image (continuous_comp M)) closed
+  refine' IsCompact.of_isClosed_subset ((_ : IsCompact (F ⁻¹' A)).image (continuous_comp M)) closed
       fun f hf => _
   · haveI : CompactSpace s := isCompact_iff_compactSpace.1 hs
     refine' arzela_ascoli₁ _ (continuous_iff_isClosed.1 (continuous_comp M) _ closed) _
diff --git a/Mathlib/Topology/ContinuousFunction/CocompactMap.lean b/Mathlib/Topology/ContinuousFunction/CocompactMap.lean
@@ -195,7 +195,7 @@ theorem isCompact_preimage [T2Space β] (f : CocompactMap α β) ⦃s : Set β
             (cocompact_tendsto f <|
               mem_cocompact.mpr ⟨s, hs, compl_subset_compl.mpr (image_preimage_subset f _)⟩))
   exact
-    isCompact_of_isClosed_subset ht (hs.isClosed.preimage <| map_continuous f) (by simpa using hts)
+    ht.of_isClosed_subset (hs.isClosed.preimage <| map_continuous f) (by simpa using hts)
 #align cocompact_map.is_compact_preimage CocompactMap.isCompact_preimage
 
 end Basics
diff --git a/Mathlib/Topology/MetricSpace/Basic.lean b/Mathlib/Topology/MetricSpace/Basic.lean
@@ -1953,7 +1953,7 @@ lemma eventually_isCompact_closedBall [LocallyCompactSpace α] (x : α) :
     ∀ᶠ r in 𝓝 (0 : ℝ), IsCompact (closedBall x r) := by
   rcases local_compact_nhds (x := x) (n := univ) univ_mem with ⟨s, hs, -, s_compact⟩
   filter_upwards [eventually_closedBall_subset hs] with r hr
-  exact isCompact_of_isClosed_subset s_compact isClosed_ball hr
+  exact IsCompact.of_isClosed_subset s_compact isClosed_ball hr
 
 lemma exists_isCompact_closedBall [LocallyCompactSpace α] (x : α) :
     ∃ r, 0 < r ∧ IsCompact (closedBall x r) := by
@@ -2204,7 +2204,7 @@ export ProperSpace (isCompact_closedBall)
 /-- In a proper pseudometric space, all spheres are compact. -/
 theorem isCompact_sphere {α : Type*} [PseudoMetricSpace α] [ProperSpace α] (x : α) (r : ℝ) :
     IsCompact (sphere x r) :=
-  isCompact_of_isClosed_subset (isCompact_closedBall x r) isClosed_sphere sphere_subset_closedBall
+  (isCompact_closedBall x r).of_isClosed_subset isClosed_sphere sphere_subset_closedBall
 #align is_compact_sphere isCompact_sphere
 
 /-- In a proper pseudometric space, any sphere is a `CompactSpace` when considered as a subtype. -/
@@ -2239,7 +2239,7 @@ theorem tendsto_dist_left_cocompact_atTop [ProperSpace α] (x : α) :
 useful when the lower bound for the radius is 0. -/
 theorem properSpace_of_compact_closedBall_of_le (R : ℝ)
     (h : ∀ x : α, ∀ r, R ≤ r → IsCompact (closedBall x r)) : ProperSpace α :=
-  ⟨fun x r => isCompact_of_isClosed_subset (h x (max r R) (le_max_right _ _)) isClosed_ball
+  ⟨fun x r => IsCompact.of_isClosed_subset (h x (max r R) (le_max_right _ _)) isClosed_ball
     (closedBall_subset_closedBall <| le_max_left _ _)⟩
 #align proper_space_of_compact_closed_ball_of_le properSpace_of_compact_closedBall_of_le
 
@@ -2298,8 +2298,7 @@ theorem exists_pos_lt_subset_ball (hr : 0 < r) (hs : IsClosed s) (h : s ⊆ ball
   rcases eq_empty_or_nonempty s with (rfl | hne)
   · exact ⟨r / 2, ⟨half_pos hr, half_lt_self hr⟩, empty_subset _⟩
   have : IsCompact s :=
-    isCompact_of_isClosed_subset (isCompact_closedBall x r) hs
-      (h.trans ball_subset_closedBall)
+    (isCompact_closedBall x r).of_isClosed_subset hs (h.trans ball_subset_closedBall)
   obtain ⟨y, hys, hy⟩ : ∃ y ∈ s, s ⊆ closedBall x (dist y x) :=
     this.exists_forall_ge hne (continuous_id.dist continuous_const).continuousOn
   have hyr : dist y x < r := h hys
@@ -2558,7 +2557,7 @@ theorem isCompact_of_isClosed_isBounded [ProperSpace α] (hc : IsClosed s) (hb :
   rcases eq_empty_or_nonempty s with (rfl | ⟨x, -⟩)
   · exact isCompact_empty
   · rcases hb.subset_closedBall x with ⟨r, hr⟩
-    exact isCompact_of_isClosed_subset (isCompact_closedBall x r) hc hr
+    exact (isCompact_closedBall x r).of_isClosed_subset hc hr
 #align metric.is_compact_of_is_closed_bounded Metric.isCompact_of_isClosed_isBounded
 
 /-- The **Heine–Borel theorem**: In a proper space, the closure of a bounded set is compact. -/
diff --git a/Mathlib/Topology/MetricSpace/HausdorffDistance.lean b/Mathlib/Topology/MetricSpace/HausdorffDistance.lean
@@ -1299,7 +1299,7 @@ theorem _root_.IsCompact.exists_isCompact_cthickening [LocallyCompactSpace α] (
   rcases exists_compact_superset hs with ⟨K, K_compact, hK⟩
   rcases hs.exists_cthickening_subset_open isOpen_interior hK with ⟨δ, δpos, hδ⟩
   refine ⟨δ, δpos, ?_⟩
-  exact isCompact_of_isClosed_subset K_compact isClosed_cthickening (hδ.trans interior_subset)
+  exact K_compact.of_isClosed_subset isClosed_cthickening (hδ.trans interior_subset)
 
 theorem _root_.IsCompact.exists_thickening_subset_open (hs : IsCompact s) (ht : IsOpen t)
     (hst : s ⊆ t) : ∃ δ, 0 < δ ∧ thickening δ s ⊆ t :=
diff --git a/Mathlib/Topology/ProperMap.lean b/Mathlib/Topology/ProperMap.lean
@@ -237,7 +237,7 @@ lemma isProperMap_iff_isClosedMap_and_tendsto_cofinite [T1Space Y] :
   refine and_congr_right fun f_cont ↦ and_congr_right fun _ ↦
     ⟨fun H y ↦ (H y).compl_mem_cocompact, fun H y ↦ ?_⟩
   rcases mem_cocompact.mp (H y) with ⟨K, hK, hKy⟩
-  exact isCompact_of_isClosed_subset hK (isClosed_singleton.preimage f_cont)
+  exact hK.of_isClosed_subset (isClosed_singleton.preimage f_cont)
     (compl_le_compl_iff_le.mp hKy)
 
 /-- A continuous map from a compact space to a T₂ space is a proper map. -/
@@ -272,7 +272,7 @@ lemma isProperMap_iff_tendsto_cocompact [T2Space Y] [WeaklyLocallyCompactSpace Y
   refine and_congr_right fun f_cont ↦
     ⟨fun H K hK ↦ (H hK).compl_mem_cocompact, fun H K hK ↦ ?_⟩
   rcases mem_cocompact.mp (H K hK) with ⟨K', hK', hK'y⟩
-  exact isCompact_of_isClosed_subset hK' (hK.isClosed.preimage f_cont)
+  exact hK'.of_isClosed_subset (hK.isClosed.preimage f_cont)
     (compl_le_compl_iff_le.mp hK'y)
 
 /-- A proper map `f : X → Y` is **universally closed**: for any topological space `Z`, the map
diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean
@@ -461,7 +461,7 @@ theorem Bornology.relativelyCompact.isBounded_iff [T1Space α] {s : Set α} :
   constructor
   · rintro ⟨t, ht₁, ht₂, hst⟩
     rw [compl_subset_compl] at hst
-    exact isCompact_of_isClosed_subset ht₂ isClosed_closure (closure_minimal hst ht₁)
+    exact ht₂.of_isClosed_subset isClosed_closure (closure_minimal hst ht₁)
   · intro h
     exact ⟨closure s, isClosed_closure, h, compl_subset_compl.mpr subset_closure⟩
 #align bornology.relatively_compact.is_bounded_iff Bornology.relativelyCompact.isBounded_iff
@@ -1343,7 +1343,7 @@ theorem IsCompact.inter [T2Space α] {s t : Set α} (hs : IsCompact s) (ht : IsC
 
 theorem isCompact_closure_of_subset_compact [T2Space α] {s t : Set α} (ht : IsCompact t)
     (h : s ⊆ t) : IsCompact (closure s) :=
-  isCompact_of_isClosed_subset ht isClosed_closure (closure_minimal h ht.isClosed)
+  ht.of_isClosed_subset isClosed_closure (closure_minimal h ht.isClosed)
 #align is_compact_closure_of_subset_compact isCompact_closure_of_subset_compact
 
 @[simp]
diff --git a/Mathlib/Topology/SubsetProperties.lean b/Mathlib/Topology/SubsetProperties.lean
@@ -128,10 +128,10 @@ theorem IsCompact.diff (hs : IsCompact s) (ht : IsOpen t) : IsCompact (s \ t) :=
 #align is_compact.diff IsCompact.diff
 
 /-- A closed subset of a compact set is a compact set. -/
-theorem isCompact_of_isClosed_subset (hs : IsCompact s) (ht : IsClosed t) (h : t ⊆ s) :
+theorem IsCompact.of_isClosed_subset (hs : IsCompact s) (ht : IsClosed t) (h : t ⊆ s) :
     IsCompact t :=
   inter_eq_self_of_subset_right h ▸ hs.inter_right ht
-#align is_compact_of_is_closed_subset isCompact_of_isClosed_subset
+#align is_compact_of_is_closed_subset IsCompact.of_isClosed_subset
 
 theorem IsCompact.image_of_continuousOn {f : α → β} (hs : IsCompact s) (hf : ContinuousOn f s) :
     IsCompact (f '' s) := by
@@ -306,7 +306,7 @@ theorem IsCompact.nonempty_iInter_of_sequence_nonempty_compact_closed (Z : ℕ 
   have Zmono : Antitone Z := antitone_nat_of_succ_le hZd
   have hZd : Directed (· ⊇ ·) Z := directed_of_sup Zmono
   have : ∀ i, Z i ⊆ Z 0 := fun i => Zmono <| zero_le i
-  have hZc : ∀ i, IsCompact (Z i) := fun i => isCompact_of_isClosed_subset hZ0 (hZcl i) (this i)
+  have hZc : ∀ i, IsCompact (Z i) := fun i => hZ0.of_isClosed_subset (hZcl i) (this i)
   IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed Z hZd hZn hZc hZcl
 #align is_compact.nonempty_Inter_of_sequence_nonempty_compact_closed IsCompact.nonempty_iInter_of_sequence_nonempty_compact_closed
 
@@ -733,7 +733,7 @@ theorem compactSpace_of_finite_subfamily_closed
 #align compact_space_of_finite_subfamily_closed compactSpace_of_finite_subfamily_closed
 
 theorem IsClosed.isCompact [CompactSpace α] {s : Set α} (h : IsClosed s) : IsCompact s :=
-  isCompact_of_isClosed_subset isCompact_univ h (subset_univ _)
+  isCompact_univ.of_isClosed_subset h (subset_univ _)
 #align is_closed.is_compact IsClosed.isCompact
 
 /-- `α` is a noncompact topological space if it is not a compact space. -/
diff --git a/Mathlib/Topology/Support.lean b/Mathlib/Topology/Support.lean
