English
Equality of two distributive actions structures parametrized by M and the same data holds by reflexivity.
Русский
Свойства равенства структур действия над M выполняются по рефлексивности.
LaTeX
$$$\\text{congr\_simp} : \\operatorname{Eq}(\\mathrm{UniformConvergenceCLM}.\\mathrm{instDistribMulAction}(\\sigma,F,M,\\mathcal{S}), \\mathrm{UniformConvergenceCLM}.\\mathrm{instDistribMulAction}(\\sigma,F,M,\\mathcal{S}))$$$
Lean4
theorem continuousSMul [RingHomSurjective σ] [RingHomIsometric σ] [TopologicalSpace F] [IsTopologicalAddGroup F]
[ContinuousSMul 𝕜₂ F] (𝔖 : Set (Set E)) (h𝔖₃ : ∀ S ∈ 𝔖, IsVonNBounded 𝕜₁ S) :
ContinuousSMul 𝕜₂ (UniformConvergenceCLM σ F 𝔖) :=
by
letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
let φ : (UniformConvergenceCLM σ F 𝔖) →ₗ[𝕜₂] E → F := ⟨⟨DFunLike.coe, fun _ _ => rfl⟩, fun _ _ => rfl⟩
exact
UniformOnFun.continuousSMul_induced_of_image_bounded 𝕜₂ E F (UniformConvergenceCLM σ F 𝔖) φ ⟨rfl⟩ fun u s hs =>
(h𝔖₃ s hs).image u
