zero_or_exists_apply_eq_finset_sup

English

If s is nonempty, there exists i in s such that s.sup p x = p_i x.

Русский

Если множество индексов s непустое, существует i ∈ s с равенством s.sup p x = p_i x.

LaTeX

$$$\exists i \in s\;\text{with}\; s.sup p x = p_i x$$$

Lean4

theorem zero_or_exists_apply_eq_finset_sup (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E) :
    s.sup p x = 0 ∨ ∃ i ∈ s, s.sup p x = p i x :=
  by
  rcases Finset.eq_empty_or_nonempty s with (rfl | hs)
  · left; rfl
  · right; exact exists_apply_eq_finset_sup p hs x

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