instIsTopologicalAddGroup

Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

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

English

The weak operator topology space E →WOT 𝕜 F is an uniform additive group.

Русский

Пространство слабой операторной топологии образует униформную группу по сложению.

LaTeX

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

Lean4

instance instIsTopologicalAddGroup : IsTopologicalAddGroup (E →WOT[𝕜] F) where toContinuousAdd := inferInstance

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

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

Разделы

Аффилиация

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