continuousSMul

Mathlib.Analysis.LocallyConvex.WithSeminorms

URI: https://scilib.ai/kg/mathlib#WithSeminorms.continuousSMul

English

The topology induced by p makes E a topological additive group.

Русский

Топология, порождённая p, делает E топологической аддитивной группой.

LaTeX

$$WithSeminorms p → IsTopologicalAddGroup E$$

Lean4

theorem continuousSMul (hp : WithSeminorms p) : ContinuousSMul 𝕜 E :=
  by
  rw [hp.withSeminorms_eq]
  exact ModuleFilterBasis.continuousSMul _

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

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

Разделы

Аффилиация

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