instContinuousAdd

Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

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

English

The addition on the weak operator topology space E →WOT 𝕜 F is continuous.

Русский

Сложение в пространстве E →WOT 𝕜 F непрерывно относительно топологии слабой операторной.

LaTeX

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

Lean4

instance instContinuousAdd : ContinuousAdd (E →WOT[𝕜] F) :=
  .induced (inducingFn 𝕜 E F)

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

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

Разделы

Аффилиация

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