coe_sSup_eq — Mathlib

English

If s is bounded above, the function-coercion of the supremum equals the supremum of the coerced functions.

Русский

Если множество ограничено сверху, отображение верхнего смысла совпадает со свёрткой над функциями.

LaTeX

$$$\uparrow(sSup s) = \bigsqcup_{p\in s} (p)$$$

Lean4

protected theorem coe_sSup_eq {s : Set <| Seminorm 𝕜 E} (hs : BddAbove s) :
    ↑(sSup s) = ⨆ p : s, ((p : Seminorm 𝕜 E) : E → ℝ) :=
  Seminorm.coe_sSup_eq' (Seminorm.bddAbove_iff.mp hs)

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