fix: rename HasContinuousConstSMul to ContinuousConstSMul (#2185)

Mathlib/Dynamics/Minimal.lean

@@ -93,7 +93,7 @@ theorem IsOpen.unionᵢ_smul [IsMinimal G α] {U : Set α} (hUo : IsOpen U) (hne
 #align is_open.Union_vadd IsOpen.unionᵢ_vadd
 
 @[to_additive]
-theorem IsCompact.exists_finite_cover_smul [IsMinimal G α] [HasContinuousConstSMul G α]
+theorem IsCompact.exists_finite_cover_smul [IsMinimal G α] [ContinuousConstSMul G α]
     {K U : Set α} (hK : IsCompact K) (hUo : IsOpen U) (hne : U.Nonempty) :
     ∃ I : Finset G, K ⊆ ⋃ g ∈ I, g • U :=
   (hK.elim_finite_subcover (fun g ↦ g • U) fun _ ↦ hUo.smul _) <| calc
@@ -119,7 +119,7 @@ theorem eq_empty_or_univ_of_smul_invariant_closed [IsMinimal M α] {s : Set α}
 #align eq_empty_or_univ_of_vadd_invariant_closed eq_empty_or_univ_of_vadd_invariant_closed
 
 @[to_additive]
-theorem isMinimal_iff_closed_smul_invariant [HasContinuousConstSMul M α] :
+theorem isMinimal_iff_closed_smul_invariant [ContinuousConstSMul M α] :
     IsMinimal M α ↔ ∀ s : Set α, IsClosed s → (∀ c : M, c • s ⊆ s) → s = ∅ ∨ s = univ := by
   constructor
   · intro _ _

Mathlib/Topology/Algebra/ConstMulAction.lean

@@ -17,13 +17,13 @@ import Mathlib.Topology.Support
 /-!
 # Monoid actions continuous in the second variable
 
-In this file we define class `HasContinuousConstSMul`. We say `HasContinuousConstSMul Γ T` if
+In this file we define class `ContinuousConstSMul`. We say `ContinuousConstSMul Γ T` if
 `Γ` acts on `T` and for each `γ`, the map `x ↦ γ • x` is continuous. (This differs from
-`HasContinuousSMul`, which requires simultaneous continuity in both variables.)
+`ContinuousSMul`, which requires simultaneous continuity in both variables.)
 
 ## Main definitions
 
-* `HasContinuousConstSMul Γ T` : typeclass saying that the map `x ↦ γ • x` is continuous on `T`;
+* `ContinuousConstSMul Γ T` : typeclass saying that the map `x ↦ γ • x` is continuous on `T`;
 * `ProperlyDiscontinuousSMul`: says that the scalar multiplication `(•) : Γ → T → T`
   is properly discontinuous, that is, for any pair of compact sets `K, L` in `T`, only finitely
   many `γ:Γ` move `K` to have nontrivial intersection with `L`.
@@ -47,38 +47,38 @@ open Topology Pointwise Filter Set TopologicalSpace
 
 attribute [local instance] MulAction.orbitRel
 
-/-- Class `HasContinuousConstSMul Γ T` says that the scalar multiplication `(•) : Γ → T → T`
+/-- Class `ContinuousConstSMul Γ T` says that the scalar multiplication `(•) : Γ → T → T`
 is continuous in the second argument. We use the same class for all kinds of multiplicative
 actions, including (semi)modules and algebras.
 
-Note that both `HasContinuousConstSMul α α` and `HasContinuousConstSMul αᵐᵒᵖ α` are
-weaker versions of `HasContinuousMul α`. -/
-class HasContinuousConstSMul (Γ : Type _) (T : Type _) [TopologicalSpace T] [SMul Γ T] : Prop where
+Note that both `ContinuousConstSMul α α` and `ContinuousConstSMul αᵐᵒᵖ α` are
+weaker versions of `ContinuousMul α`. -/
+class ContinuousConstSMul (Γ : Type _) (T : Type _) [TopologicalSpace T] [SMul Γ T] : Prop where
   /-- The scalar multiplication `(•) : Γ → T → T` is continuous in the second argument. -/
   continuous_const_smul : ∀ γ : Γ, Continuous fun x : T => γ • x
-#align has_continuous_const_smul HasContinuousConstSMul
+#align has_continuous_const_smul ContinuousConstSMul
 
-/-- Class `HasContinuousConstVAdd Γ T` says that the additive action `(+ᵥ) : Γ → T → T`
+/-- Class `ContinuousConstVAdd Γ T` says that the additive action `(+ᵥ) : Γ → T → T`
 is continuous in the second argument. We use the same class for all kinds of additive actions,
 including (semi)modules and algebras.
 
-Note that both `HasContinuousConstVAdd α α` and `HasContinuousConstVAdd αᵐᵒᵖ α` are
-weaker versions of `HasContinuousVAdd α`. -/
-class HasContinuousConstVAdd (Γ : Type _) (T : Type _) [TopologicalSpace T] [VAdd Γ T] : Prop where
+Note that both `ContinuousConstVAdd α α` and `ContinuousConstVAdd αᵐᵒᵖ α` are
+weaker versions of `ContinuousVAdd α`. -/
+class ContinuousConstVAdd (Γ : Type _) (T : Type _) [TopologicalSpace T] [VAdd Γ T] : Prop where
   /-- The additive action `(+ᵥ) : Γ → T → T` is continuous in the second argument. -/
   continuous_const_vadd : ∀ γ : Γ, Continuous fun x : T => γ +ᵥ x
-#align has_continuous_const_vadd HasContinuousConstVAdd
+#align has_continuous_const_vadd ContinuousConstVAdd
 
-attribute [to_additive] HasContinuousConstSMul
+attribute [to_additive] ContinuousConstSMul
 
-export HasContinuousConstSMul (continuous_const_smul)
-export HasContinuousConstVAdd (continuous_const_vadd)
+export ContinuousConstSMul (continuous_const_smul)
+export ContinuousConstVAdd (continuous_const_vadd)
 
 variable {M α β : Type _}
 
 section SMul
 
-variable [TopologicalSpace α] [SMul M α] [HasContinuousConstSMul M α]
+variable [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α]
 
 @[to_additive]
 theorem Filter.Tendsto.const_smul {f : β → α} {l : Filter β} {a : α} (hf : Tendsto f l (𝓝 a))
@@ -118,38 +118,38 @@ theorem Continuous.const_smul (hg : Continuous g) (c : M) : Continuous fun x =>
 /-- If a scalar is central, then its right action is continuous when its left action is. -/
 @[to_additive "If an additive action is central, then its right action is continuous when its left
 action is."]
-instance HasContinuousConstSMul.op [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] :
-    HasContinuousConstSMul Mᵐᵒᵖ α :=
+instance ContinuousConstSMul.op [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] :
+    ContinuousConstSMul Mᵐᵒᵖ α :=
   ⟨MulOpposite.rec' fun c => by simpa only [op_smul_eq_smul] using continuous_const_smul c⟩
-#align has_continuous_const_smul.op HasContinuousConstSMul.op
-#align has_continuous_const_vadd.op HasContinuousConstVAdd.op
+#align has_continuous_const_smul.op ContinuousConstSMul.op
+#align has_continuous_const_vadd.op ContinuousConstVAdd.op
 
 @[to_additive]
-instance MulOpposite.hasContinuousConstSMul : HasContinuousConstSMul M αᵐᵒᵖ :=
+instance MulOpposite.continuousConstSMul : ContinuousConstSMul M αᵐᵒᵖ :=
   ⟨fun c => MulOpposite.continuous_op.comp <| MulOpposite.continuous_unop.const_smul c⟩
-#align mul_opposite.has_continuous_const_smul MulOpposite.hasContinuousConstSMul
-#align add_opposite.has_continuous_const_vadd AddOpposite.hasContinuousConstVAdd
+#align mul_opposite.has_continuous_const_smul MulOpposite.continuousConstSMul
+#align add_opposite.has_continuous_const_vadd AddOpposite.continuousConstVAdd
 
 @[to_additive]
-instance : HasContinuousConstSMul M αᵒᵈ := ‹HasContinuousConstSMul M α›
+instance : ContinuousConstSMul M αᵒᵈ := ‹ContinuousConstSMul M α›
 
 @[to_additive]
-instance OrderDual.hasContinuousConstSMul' : HasContinuousConstSMul Mᵒᵈ α :=
-  ‹HasContinuousConstSMul M α›
-#align order_dual.has_continuous_const_smul' OrderDual.hasContinuousConstSMul'
-#align order_dual.has_continuous_const_vadd' OrderDual.hasContinuousConstVAdd'
+instance OrderDual.continuousConstSMul' : ContinuousConstSMul Mᵒᵈ α :=
+  ‹ContinuousConstSMul M α›
+#align order_dual.has_continuous_const_smul' OrderDual.continuousConstSMul'
+#align order_dual.has_continuous_const_vadd' OrderDual.continuousConstVAdd'
 
 @[to_additive]
-instance [SMul M β] [HasContinuousConstSMul M β] : HasContinuousConstSMul M (α × β) :=
+instance [SMul M β] [ContinuousConstSMul M β] : ContinuousConstSMul M (α × β) :=
   ⟨fun _ => (continuous_fst.const_smul _).prod_mk (continuous_snd.const_smul _)⟩
 
 @[to_additive]
 instance {ι : Type _} {γ : ι → Type _} [∀ i, TopologicalSpace (γ i)] [∀ i, SMul M (γ i)]
-    [∀ i, HasContinuousConstSMul M (γ i)] : HasContinuousConstSMul M (∀ i, γ i) :=
+    [∀ i, ContinuousConstSMul M (γ i)] : ContinuousConstSMul M (∀ i, γ i) :=
   ⟨fun _ => continuous_pi fun i => (continuous_apply i).const_smul _⟩
 
 @[to_additive]
-theorem IsCompact.smul {α β} [SMul α β] [TopologicalSpace β] [HasContinuousConstSMul α β] (a : α)
+theorem IsCompact.smul {α β} [SMul α β] [TopologicalSpace β] [ContinuousConstSMul α β] (a : α)
     {s : Set β} (hs : IsCompact s) : IsCompact (a • s) :=
   hs.image (continuous_id.const_smul a)
 #align is_compact.smul IsCompact.smul
@@ -161,13 +161,13 @@ section Monoid
 
 variable [TopologicalSpace α]
 
-variable [Monoid M] [MulAction M α] [HasContinuousConstSMul M α]
+variable [Monoid M] [MulAction M α] [ContinuousConstSMul M α]
 
 @[to_additive]
-instance Units.hasContinuousConstSMul : HasContinuousConstSMul Mˣ α
+instance Units.continuousConstSMul : ContinuousConstSMul Mˣ α
     where continuous_const_smul m := (continuous_const_smul (m : M) : _)
-#align units.has_continuous_const_smul Units.hasContinuousConstSMul
-#align add_units.has_continuous_const_vadd AddUnits.hasContinuousConstVAdd
+#align units.has_continuous_const_smul Units.continuousConstSMul
+#align add_units.has_continuous_const_vadd AddUnits.continuousConstVAdd
 
 @[to_additive]
 theorem smul_closure_subset (c : M) (s : Set α) : c • closure s ⊆ closure (c • s) :=
@@ -186,7 +186,7 @@ end Monoid
 
 section Group
 
-variable {G : Type _} [TopologicalSpace α] [Group G] [MulAction G α] [HasContinuousConstSMul G α]
+variable {G : Type _} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α]
 
 @[to_additive]
 theorem tendsto_const_smul_iff {f : β → α} {l : Filter β} {a : α} (c : G) :
@@ -285,7 +285,7 @@ end Group
 section GroupWithZero
 
 variable {G₀ : Type _} [TopologicalSpace α] [GroupWithZero G₀] [MulAction G₀ α]
-  [HasContinuousConstSMul G₀ α]
+  [ContinuousConstSMul G₀ α]
 
 theorem tendsto_const_smul_iff₀ {f : β → α} {l : Filter β} {a : α} {c : G₀} (hc : c ≠ 0) :
     Tendsto (fun x => c • f x) l (𝓝 <| c • a) ↔ Tendsto f l (𝓝 a) :=
@@ -332,7 +332,7 @@ theorem interior_smul₀ {c : G₀} (hc : c ≠ 0) (s : Set α) : interior (c 
 #align interior_smul₀ interior_smul₀
 
 theorem closure_smul₀ {E} [Zero E] [MulActionWithZero G₀ E] [TopologicalSpace E] [T1Space E]
-    [HasContinuousConstSMul G₀ E] (c : G₀) (s : Set E) : closure (c • s) = c • closure s := by
+    [ContinuousConstSMul G₀ E] (c : G₀) (s : Set E) : closure (c • s) = c • closure s := by
   rcases eq_or_ne c 0 with (rfl | hc)
   · rcases eq_empty_or_nonempty s with (rfl | hs)
     · simp
@@ -359,7 +359,7 @@ theorem IsClosed.smul_of_ne_zero {c : G₀} {s : Set α} (hs : IsClosed s) (hc :
 The lemma that `smul` is a closed map in the first argument (for a normed space over a complete
 normed field) is `isClosedMap_smul_left` in `Analysis.NormedSpace.FiniteDimension`. -/
 theorem isClosedMap_smul₀ {𝕜 M : Type _} [DivisionRing 𝕜] [AddCommMonoid M] [TopologicalSpace M]
-    [T1Space M] [Module 𝕜 M] [HasContinuousConstSMul 𝕜 M] (c : 𝕜) :
+    [T1Space M] [Module 𝕜 M] [ContinuousConstSMul 𝕜 M] (c : 𝕜) :
     IsClosedMap fun x : M => c • x := by
   rcases eq_or_ne c 0 with (rfl | hne)
   · simp only [zero_smul]
@@ -368,7 +368,7 @@ theorem isClosedMap_smul₀ {𝕜 M : Type _} [DivisionRing 𝕜] [AddCommMonoid
 #align is_closed_map_smul₀ isClosedMap_smul₀
 
 theorem IsClosed.smul₀ {𝕜 M : Type _} [DivisionRing 𝕜] [AddCommMonoid M] [TopologicalSpace M]
-    [T1Space M] [Module 𝕜 M] [HasContinuousConstSMul 𝕜 M] (c : 𝕜) {s : Set M} (hs : IsClosed s) :
+    [T1Space M] [Module 𝕜 M] [ContinuousConstSMul 𝕜 M] (c : 𝕜) {s : Set M} (hs : IsClosed s) :
     IsClosed (c • s) :=
   isClosedMap_smul₀ c s hs
 #align is_closed.smul₀ IsClosed.smul₀
@@ -389,7 +389,7 @@ end GroupWithZero
 
 namespace IsUnit
 
-variable [Monoid M] [TopologicalSpace α] [MulAction M α] [HasContinuousConstSMul M α]
+variable [Monoid M] [TopologicalSpace α] [MulAction M α] [ContinuousConstSMul M α]
 
 nonrec theorem tendsto_const_smul_iff {f : β → α} {l : Filter β} {a : α} {c : M} (hc : IsUnit c) :
     Tendsto (fun x => c • f x) l (𝓝 <| c • a) ↔ Tendsto f l (𝓝 a) :=
@@ -476,7 +476,7 @@ export ProperlyDiscontinuousVAdd (finite_disjoint_inter_image)
   quotient. -/
 @[to_additive "The quotient map by a group action is open, i.e. the quotient by a group
 action is an open quotient. "]
-theorem isOpenMap_quotient_mk'_mul [HasContinuousConstSMul Γ T] :
+theorem isOpenMap_quotient_mk'_mul [ContinuousConstSMul Γ T] :
     IsOpenMap (Quotient.mk' : T → Quotient (MulAction.orbitRel Γ T)) := fun U hU => by
   rw [isOpen_coinduced, MulAction.quotient_preimage_image_eq_union_mul U]
   exact isOpen_unionᵢ fun γ => isOpenMap_smul γ U hU
@@ -487,7 +487,7 @@ theorem isOpenMap_quotient_mk'_mul [HasContinuousConstSMul Γ T] :
 @[to_additive "The quotient by a discontinuous group action of a locally compact t2
 space is t2."]
 instance (priority := 100) t2Space_of_properlyDiscontinuousSMul_of_t2Space [T2Space T]
-    [LocallyCompactSpace T] [HasContinuousConstSMul Γ T] [ProperlyDiscontinuousSMul Γ T] :
+    [LocallyCompactSpace T] [ContinuousConstSMul Γ T] [ProperlyDiscontinuousSMul Γ T] :
     T2Space (Quotient (MulAction.orbitRel Γ T)) := by
   set Q := Quotient (MulAction.orbitRel Γ T)
   rw [t2Space_iff_nhds]
@@ -523,18 +523,18 @@ instance (priority := 100) t2Space_of_properlyDiscontinuousSMul_of_t2Space [T2Sp
 /-- The quotient of a second countable space by a group action is second countable. -/
 @[to_additive "The quotient of a second countable space by an additive group action is second
 countable."]
-theorem HasContinuousConstSMul.secondCountableTopology [SecondCountableTopology T]
-    [HasContinuousConstSMul Γ T] : SecondCountableTopology (Quotient (MulAction.orbitRel Γ T)) :=
+theorem ContinuousConstSMul.secondCountableTopology [SecondCountableTopology T]
+    [ContinuousConstSMul Γ T] : SecondCountableTopology (Quotient (MulAction.orbitRel Γ T)) :=
   TopologicalSpace.Quotient.secondCountableTopology isOpenMap_quotient_mk'_mul
-#align has_continuous_const_smul.second_countable_topology HasContinuousConstSMul.secondCountableTopology
-#align has_continuous_const_vadd.second_countable_topology HasContinuousConstVAdd.secondCountableTopology
+#align has_continuous_const_smul.second_countable_topology ContinuousConstSMul.secondCountableTopology
+#align has_continuous_const_vadd.second_countable_topology ContinuousConstVAdd.secondCountableTopology
 
 section nhds
 
 section MulAction
 
 variable {G₀ : Type _} [GroupWithZero G₀] [MulAction G₀ α] [TopologicalSpace α]
-  [HasContinuousConstSMul G₀ α]
+  [ContinuousConstSMul G₀ α]
 
 -- porting note: generalize to a group action + `IsUnit`
 /-- Scalar multiplication preserves neighborhoods. -/
@@ -557,7 +557,7 @@ end MulAction
 section DistribMulAction
 
 variable {G₀ : Type _} [GroupWithZero G₀] [AddMonoid α] [DistribMulAction G₀ α] [TopologicalSpace α]
-  [HasContinuousConstSMul G₀ α]
+  [ContinuousConstSMul G₀ α]
 
 theorem set_smul_mem_nhds_zero_iff {s : Set α} {c : G₀} (hc : c ≠ 0) :
     c • s ∈ 𝓝 (0 : α) ↔ s ∈ 𝓝 (0 : α) := by