seminormAux_nonneg

Mathlib.Analysis.Distribution.SchwartzSpace

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

English

For every k, n and Schwartz map f, the seminormAux is nonnegative.

Русский

Для любых k, n и Schwartz-перехода f семинормa nonnegative.

LaTeX

$$$0 \\le f.seminormAux_{k,n}$$$

Lean4

theorem seminormAux_nonneg (k n : ℕ) (f : 𝓢(E, F)) : 0 ≤ f.seminormAux k n :=
  le_csInf (bounds_nonempty k n f) fun _ ⟨hx, _⟩ => hx

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

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

Разделы

Аффилиация

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