instIsTopologicalAddGroup

Mathlib.Topology.Algebra.Module.WeakDual

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

English

WeakSpace 𝕜 E is a topological additive group.

Русский

WeakSpace 𝕜 E является топологической аддитивной группой.

LaTeX

$$$IsTopologicalAddGroup (\\mathrm{WeakSpace } 𝕜 E)$$$

Lean4

instance instIsTopologicalAddGroup : IsTopologicalAddGroup (WeakSpace 𝕜 E) :=
  WeakBilin.instIsTopologicalAddGroup (topDualPairing 𝕜 E).flip

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

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

Разделы

Аффилиация

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