instDistribMulAction — Mathlib

English

UniformConvergenceCLM σ F 𝔖 inherits a module structure over a base ring R with compatible scalar action

Русский

UniformConvergenceCLM σ F 𝔖 наследует структуру модуля над кольцом R с совместным действием скаляров

LaTeX

$$$\\text{Module } R (\\mathrm{UniformConvergenceCLM}(\\sigma,F,\\mathcal{S}))$$$

Lean4

instance instDistribMulAction (M : Type*) [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [TopologicalSpace F]
    [IsTopologicalAddGroup F] [ContinuousConstSMul M F] (𝔖 : Set (Set E)) :
    DistribMulAction M (UniformConvergenceCLM σ F 𝔖) :=
  ContinuousLinearMap.distribMulAction

Похожие утверждения