instZero

Mathlib.Analysis.Distribution.SchwartzSpace

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

English

The seminorm of a sum is bounded by the sum of seminorms.

Русский

Семинормa суммы ограничена суммой семинорм.

LaTeX

$$$ (f+g).seminormAux_{k,n} \\le f.seminormAux_{k,n} + g.seminormAux_{k,n} $$$

Lean4

instance instZero : Zero 𝓢(E, F) :=
  ⟨{  toFun := fun _ => 0
      smooth' := contDiff_const
      decay' := fun _ _ => ⟨1, fun _ => by simp⟩ }⟩

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

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

Разделы

Аффилиация

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