English
For a nonempty finite index set, the closedBall of the supremum equals the infimum of the individual closedBalls: closedBall (s.sup' H p) e r = s.inf' H (i ↦ closedBall (p i) e r).
Русский
Для непустого конечного индекса замкнутый шар супремума равен инфимуму замкнутых шаров по каждому индексу.
LaTeX
$$$\\mathrm{closedBall}_{s.sup' H p}(e,r) = \\inf' H\\; (i \\mapsto \\mathrm{closedBall}_{p_i}(e,r))$$$
Lean4
theorem closedBall_finset_sup' (p : ι → Seminorm 𝕜 E) (s : Finset ι) (H : s.Nonempty) (e : E) (r : ℝ) :
closedBall (s.sup' H p) e r = s.inf' H fun i => closedBall (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, closedBall_sup, inf_eq_inter, ih]
