finset_sup_apply_le — Mathlib

English

There exists i ∈ s such that s.sup p x = p_i x, when s.Nonempty.

Русский

Существует i ∈ s такое, что s.sup p x = p_i x, если s непусто.

LaTeX

$$$\exists i \in s,\; s.sup p x = p_i x$$$

Lean4

theorem finset_sup_apply_le {p : ι → Seminorm 𝕜 E} {s : Finset ι} {x : E} {a : ℝ} (ha : 0 ≤ a)
    (h : ∀ i, i ∈ s → p i x ≤ a) : s.sup p x ≤ a :=
  by
  lift a to ℝ≥0 using ha
  rw [finset_sup_apply, NNReal.coe_le_coe]
  exact Finset.sup_le h

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