English
The value of the finite supremum of seminorms at x is the supremum of the corresponding values p_i(x) across i in s.
Русский
Значение конечного супремума семинорм в точке x равно супремуму значений p_i(x) по i∈s.
LaTeX
$$$(s \ sup p)(x) = \sup_{i \in s} p_i(x)$$$
Lean4
theorem finset_sup_apply (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E) :
s.sup p x = ↑(s.sup fun i => ⟨p i x, apply_nonneg (p i) x⟩ : ℝ≥0) := by
induction s using Finset.cons_induction_on with
| empty =>
rw [Finset.sup_empty, Finset.sup_empty, coe_bot, _root_.bot_eq_zero, Pi.zero_apply]
norm_cast
| cons a s ha ih => rw [Finset.sup_cons, Finset.sup_cons, coe_sup, Pi.sup_apply, NNReal.coe_max, NNReal.coe_mk, ih]
