finset_sup_smul — Mathlib

English

For any finite index set, either the supremum at x is zero or there exists an index i in s with s.sup p x = p_i x.

Русский

Для любого конечного множества индексов либо супремум в x равен нулю, либо существует i∈s такой, что s.sup p x = p_i x.

LaTeX

$$$s.sup p x = 0\;\text{ или }\; \exists i \in s,\; s.sup p x = p_i x$$$

Lean4

theorem finset_sup_smul (p : ι → Seminorm 𝕜 E) (s : Finset ι) (C : ℝ≥0) : s.sup (C • p) = C • s.sup p :=
  by
  ext x
  rw [smul_apply, finset_sup_apply, finset_sup_apply]
  symm
  exact congr_arg ((↑) : ℝ≥0 → ℝ) (NNReal.mul_finset_sup C s (fun i ↦ ⟨p i x, apply_nonneg _ _⟩))

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