iSup_apply — Mathlib

English

If a family {p_i} of seminorms on E is bounded above, then for each x in E, the value of the pointwise supremum equals the supremum of the values: (sup_i p_i)(x) = sup_i p_i(x).

Русский

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

LaTeX

$$$\\left(\\sup_i p_i\\right)(x) = \\sup_i p_i(x) $$$

Lean4

protected theorem iSup_apply {ι : Sort*} {p : ι → Seminorm 𝕜 E} (hp : BddAbove (range p)) {x : E} :
    (⨆ i, p i) x = ⨆ i, p i x := by rw [Seminorm.coe_iSup_eq hp, iSup_apply]

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