instContinuousSMul

Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMapWOT.instContinuousSMul

English

Scalar multiplication by 𝕜 is continuous on the weak operator topology space E →WOT 𝕜 F.

Русский

Умножение на скаляры в 𝕜 непрерывно на пространстве слабой операторной топологии.

LaTeX

$$ContinuousSMul 𝕜 (E →WOT[𝕜] F)$$

Lean4

instance instContinuousSMul : ContinuousSMul 𝕜 (E →WOT[𝕜] F) :=
  .induced (inducingFn 𝕜 E F)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru