English
For a nonempty finite set of seminorms, the ball of the supremum equals the intersection of the individual balls: ball (s.sup' H p) e r = s.inf' H (i ↦ ball (p i) e r).
Русский
Для непустого конечного набора семинорм шар супремумa равен пересечению шаров по каждому индексу.
LaTeX
$$$\\mathrm{ball}_{s.sup' H p}(e,r) = \\inf' H\\; (i \\mapsto \\mathrm{ball}_{p_i}(e,r))$$$
Lean4
theorem ball_finset_sup' (p : ι → Seminorm 𝕜 E) (s : Finset ι) (H : s.Nonempty) (e : E) (r : ℝ) :
ball (s.sup' H p) e r = s.inf' H fun i => ball (p i) e r := by
induction H using Finset.Nonempty.cons_induction with
| singleton => simp
| cons _ _ _ hs ih => simp only [Finset.sup'_cons hs, Finset.inf'_cons hs, ball_sup, inf_eq_inter, ih]
