instIsUniformAddGroup

Mathlib.Analysis.Distribution.SchwartzSpace

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

English

SchwartzMap forms an uniform additive group under the given uniform structure.

Русский

SchwartzMap образует равномерную аддитивную группу в данной равномерной структуре.

LaTeX

$$$\mathrm{instIsUniformAddGroup}: IsUniformAddGroup 𝓢(E,F)$$$

Lean4

instance instIsUniformAddGroup : IsUniformAddGroup 𝓢(E, F) :=
  (schwartzSeminormFamily ℝ E F).addGroupFilterBasis.isUniformAddGroup

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

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

Разделы

Аффилиация

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