instIsUniformAddGroup

Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

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

English

Second mention: the space inherits a uniform additive group structure from inducingFn.

Русский

Повторное утверждение: пространство наследует униформную структуру по сложению через inducingFn.

LaTeX

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

Lean4

instance instIsUniformAddGroup : IsUniformAddGroup (E →WOT[𝕜] F) :=
  .comap (inducingFn 𝕜 E F)

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

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

Разделы

Аффилиация

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