seminormAux_zero

Mathlib.Analysis.Distribution.SchwartzSpace

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

← MathLib Explorer

English

The seminorm of the sum is bounded by the sum of seminorms (second bound).

Русский

Неравенство семинормы суммы, второй вариант.

LaTeX

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

Lean4

theorem seminormAux_zero (k n : ℕ) : (0 : 𝓢(E, F)).seminormAux k n = 0 :=
  le_antisymm (seminormAux_le_bound k n _ rfl.le fun _ => by simp [Pi.zero_def]) (seminormAux_nonneg _ _ _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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