coe_sSup_eq' — Mathlib

English

SupSet has internal proofs mirroring sSup over sets: equational characterizations and coercions to real-valued functions.

Русский

SupSet имеет доказательства, сопоставляющие sSup над множествами и отображающие их в действительные значения.

LaTeX

$$coercion equivalences for sSup on sets$$

Lean4

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

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