feat: action on UniformOnFun is uniformly continuous (#9714)

- add `UniformInducing.uniformContinuousConstSMul`
  and its additive version;
- use it to prove that the pointwise actions
  on `α →ᵤ X` and `α →ᵤ[𝔖] X` are uniformly continuous;
- use the latter facts to prove that the pointwise action
  on `E →SL[σ] F` is uniformly continuous;
- make `M` explicit in `ContinuousLinearMap.strongTopology.continuousConstSMul`,
  drop unneeded arguments.

Mathlib/Topology/Algebra/Module/StrongTopology.lean

@@ -171,20 +171,24 @@ theorem strongTopology.hasBasis_nhds_zero [TopologicalSpace F] [TopologicalAddGr
   strongTopology.hasBasis_nhds_zero_of_basis σ F 𝔖 h𝔖₁ h𝔖₂ (𝓝 0).basis_sets
 #align continuous_linear_map.strong_topology.has_basis_nhds_zero ContinuousLinearMap.strongTopology.hasBasis_nhds_zero
 
-theorem strongTopology.continuousConstSMul {M : Type*}
+theorem strongTopology.uniformContinuousConstSMul (M : Type*)
     [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F]
-    [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousConstSMul M F] (𝔖 : Set (Set E))
-    (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (· ⊆ ·) 𝔖) :
-    @ContinuousConstSMul M (E →SL[σ] F) (strongTopology σ F 𝔖) _ := by
-  letI := strongTopology σ F 𝔖
-  haveI : TopologicalAddGroup (E →SL[σ] F) := strongTopology.topologicalAddGroup σ F 𝔖
-  refine ⟨fun c ↦ continuous_of_continuousAt_zero (DistribSMul.toAddMonoidHom _ c) ?_⟩
-  have H₁ := strongTopology.hasBasis_nhds_zero σ F _ h𝔖₁ h𝔖₂
-  have H₂ : Filter.Tendsto (c • ·) (𝓝 0 : Filter F) (𝓝 0) :=
-    (continuous_const_smul c).tendsto' 0 _ (smul_zero _)
-  rw [ContinuousAt, map_zero, H₁.tendsto_iff H₁]
-  rintro ⟨s, t⟩ ⟨hs : s ∈ 𝔖, ht : t ∈ 𝓝 0⟩
-  exact ⟨(s, (c • ·) ⁻¹' t), ⟨hs, H₂ ht⟩, fun f  ↦ _root_.id⟩
+    [UniformSpace F] [UniformAddGroup F] [UniformContinuousConstSMul M F] (𝔖 : Set (Set E)) :
+    @UniformContinuousConstSMul M (E →SL[σ] F) (strongUniformity σ F 𝔖) _ :=
+  let _ := strongUniformity σ F 𝔖
+  (strongUniformity.uniformEmbedding_coeFn σ F 𝔖).toUniformInducing.uniformContinuousConstSMul
+    fun _ _ ↦ rfl
+
+theorem strongTopology.continuousConstSMul (M : Type*)
+    [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F]
+    [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousConstSMul M F] (𝔖 : Set (Set E)) :
+    @ContinuousConstSMul M (E →SL[σ] F) (strongTopology σ F 𝔖) _ :=
+  let _ := TopologicalAddGroup.toUniformSpace F
+  have _ : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
+  let _ := strongUniformity σ F 𝔖
+  have _ := uniformContinuousConstSMul_of_continuousConstSMul M F
+  have _ := strongTopology.uniformContinuousConstSMul σ F M 𝔖
+  inferInstance
 
 end General
 
@@ -239,12 +243,16 @@ protected theorem hasBasis_nhds_zero [TopologicalSpace F] [TopologicalAddGroup F
   ContinuousLinearMap.hasBasis_nhds_zero_of_basis (𝓝 0).basis_sets
 #align continuous_linear_map.has_basis_nhds_zero ContinuousLinearMap.hasBasis_nhds_zero
 
+instance uniformContinuousConstSMul
+    {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F]
+    [UniformSpace F] [UniformAddGroup F] [UniformContinuousConstSMul M F] :
+    UniformContinuousConstSMul M (E →SL[σ] F) :=
+  strongTopology.uniformContinuousConstSMul σ F _ _
+
 instance continuousConstSMul {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F]
     [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousConstSMul M F] :
     ContinuousConstSMul M (E →SL[σ] F) :=
-  strongTopology.continuousConstSMul σ F {S | Bornology.IsVonNBounded 𝕜₁ S}
-    ⟨∅, Bornology.isVonNBounded_empty 𝕜₁ E⟩
-    (directedOn_of_sup_mem fun _ _ => Bornology.IsVonNBounded.union)
+  strongTopology.continuousConstSMul σ F _ _
 
 variable (G) [TopologicalSpace F] [TopologicalSpace G]
 

Mathlib/Topology/Algebra/UniformConvergence.lean

@@ -292,6 +292,22 @@ protected theorem UniformOnFun.hasBasis_nhds_one (𝔖 : Set <| Set α) (h𝔖
 
 end Group
 
+section ConstSMul
+
+variable (M α X : Type*) [SMul M X] [UniformSpace X] [UniformContinuousConstSMul M X]
+
+instance UniformFun.uniformContinuousConstSMul :
+    UniformContinuousConstSMul M (α →ᵤ X) where
+  uniformContinuous_const_smul c := UniformFun.postcomp_uniformContinuous <|
+    uniformContinuous_const_smul c
+
+instance UniformFunOn.uniformContinuousConstSMul {𝔖 : Set (Set α)} :
+    UniformContinuousConstSMul M (α →ᵤ[𝔖] X) where
+  uniformContinuous_const_smul c := UniformOnFun.postcomp_uniformContinuous <|
+    uniformContinuous_const_smul c
+
+end ConstSMul
+
 section Module
 
 variable (𝕜 α E H : Type*) {hom : Type*} [NormedField 𝕜] [AddCommGroup H] [Module 𝕜 H]

Mathlib/Topology/Algebra/UniformMulAction.lean

@@ -99,6 +99,14 @@ theorem UniformContinuous.const_smul [UniformContinuousConstSMul M X] {f : Y →
 #align uniform_continuous.const_smul UniformContinuous.const_smul
 #align uniform_continuous.const_vadd UniformContinuous.const_vadd
 
+@[to_additive]
+lemma UniformInducing.uniformContinuousConstSMul [SMul M Y] [UniformContinuousConstSMul M Y]
+    {f : X → Y} (hf : UniformInducing f) (hsmul : ∀ (c : M) x, f (c • x) = c • f x) :
+    UniformContinuousConstSMul M X where
+  uniformContinuous_const_smul c := by
+    simpa only [hf.uniformContinuous_iff, Function.comp_def, hsmul]
+      using hf.uniformContinuous.const_smul c
+
 /-- If a scalar action is central, then its right action is uniform continuous when its left action
 is. -/
 @[to_additive "If an additive action is central, then its right action is uniform