sup_apply

Mathlib.Analysis.Seminorm

URI: https://scilib.ai/kg/mathlib#Seminorm.sup_apply

English

The value of the supremum seminorm at x equals the supremum of the values of the two seminorms at x: (p ⊔ q) x = p x ⊔ q x.

Русский

Значение супремной полунормы в точке x равно супремуму значений двух полунорм в x: (p ⊔ q) x = p x ⊔ q x.

LaTeX

$$$ (p \sqcup q)(x) = p(x) \sqcup q(x) $$$

Lean4

theorem sup_apply (p q : Seminorm 𝕜 E) (x : E) : (p ⊔ q) x = p x ⊔ q x :=
  rfl

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

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

Разделы

Аффилиация

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