coe_sup

Mathlib.Analysis.Seminorm

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

English

The evaluation of the supremum of two seminorms is the supremum of their evaluations: (p ⊔ q)(x) = p(x) ⊔ q(x).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem coe_sup (p q : Seminorm 𝕜 E) : ⇑(p ⊔ q) = (p : E → ℝ) ⊔ (q : E → ℝ) :=
  rfl

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

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

Разделы

Аффилиация

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