le_finset_sup_apply — Mathlib

English

The value of the finite supremum over a set of seminorms equals the real supremum of their pointwise values.

Русский

Значение супремума по множеству семинорм равно супремуму точечных значений каждого.

LaTeX

$$$\text{for } s \subseteq \mathrm{Seminorm}(𝕜,E),\; (s.sup p)(x) = \sup_{p\in s} p(x)$$$

Lean4

theorem le_finset_sup_apply {p : ι → Seminorm 𝕜 E} {s : Finset ι} {x : E} {i : ι} (hi : i ∈ s) : p i x ≤ s.sup p x :=
  (Finset.le_sup hi : p i ≤ s.sup p) x

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