exists_apply_eq_finset_sup — Mathlib

English

If C ≥ 0 is a scalar, then the supremum of the scaled seminorms equals the scalar times the supremum of the original seminorms: sup_i (C • p_i) = C • sup_i p_i.

Русский

Если скаляр C≥0, то максимум по i от (C•p_i) равен C умноженному на максимум по i от p_i.

LaTeX

$$$\sup_{i\in s} (C \cdot p_i) = C \cdot \left( \sup_{i\in s} p_i \right)$$$

Lean4

theorem exists_apply_eq_finset_sup (p : ι → Seminorm 𝕜 E) {s : Finset ι} (hs : s.Nonempty) (x : E) :
    ∃ i ∈ s, s.sup p x = p i x :=
  by
  rcases Finset.exists_mem_eq_sup s hs (fun i ↦ (⟨p i x, apply_nonneg _ _⟩ : ℝ≥0)) with ⟨i, hi, hix⟩
  rw [finset_sup_apply]
  exact ⟨i, hi, congr_arg _ hix⟩

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