sSup_apply — Mathlib

English

Let S be a nonempty subset of seminorms on E that is bounded above. Then for every x in E, (sSup S)(x) equals sup over p in S of p(x).

Русский

Пусть S непустое подмножество семинормов на E, ограниченное сверху. Тогда для каждого x ∈ E выполняется (sSup S)(x) = sup_{p∈S} p(x).

LaTeX

$$$\\bigl(\\mathrm{sSup}\\,S\\bigr)(x) = \\displaystyle \\sup_{p\\in S} p(x)$$$

Lean4

protected theorem sSup_apply {s : Set (Seminorm 𝕜 E)} (hp : BddAbove s) {x : E} : (sSup s) x = ⨆ p : s, (p : E → ℝ) x :=
  by rw [Seminorm.coe_sSup_eq hp, iSup_apply]

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