English
Another formulation: under boundedness, the closed ball of the supremum seminorm equals the intersection over i of closed balls.
Русский
Другая формулировка: при ограниченности равенство замкнутых шаров верхней оболочки равному пересечению по i.
LaTeX
$$$\text{closedBall}(\!\bigsqcup_i p_i\!)(e,r)=\bigcap_i \text{closedBall}(p_i)(e,r)$$$
Lean4
theorem closedBall_iSup {ι : Sort*} {p : ι → Seminorm 𝕜 E} (hp : BddAbove (range p)) (e : E) {r : ℝ} (hr : 0 < r) :
closedBall (⨆ i, p i) e r = ⋂ i, closedBall (p i) e r :=
by
cases isEmpty_or_nonempty ι
· rw [iSup_of_empty', iInter_of_empty, Seminorm.sSup_empty]
exact closedBall_bot _ hr
· ext x
have := Seminorm.bddAbove_range_iff.mp hp (x - e)
simp only [mem_closedBall, mem_iInter, Seminorm.iSup_apply hp, ciSup_le_iff this]
