English
Let p be a function from a finite set ι to seminorms on E, S a finite subset of ι, x ∈ E, and r ≥ 0. Then ball of the finite sup equals the intersection of balls: ball( sup p ) x r = ⋂ i ∈ S, ball (p i) x r.
Русский
Пусть p : ι → Seminorm 𝕜 E; S ⊆ ι конечна; x ∈ E; r ≥ 0. Тогда ball( sup p ) x r равно пересечению шаров: ball(sup p) x r = ⋂ i ∈ S, ball(p i) x r.
LaTeX
$$$\text{ball}(\,s.\!\sup p\,)\,x\,r = \bigcap_{i \in s} \text{ball}(p i)\,x\,r$$$
Lean4
/-- Seminorm-balls at the origin are balanced. -/
theorem balanced_ball_zero (r : ℝ) : Balanced 𝕜 (ball p 0 r) :=
by
rintro a ha x ⟨y, hy, hx⟩
rw [mem_ball_zero, ← hx, map_smul_eq_mul]
calc
_ ≤ p y := mul_le_of_le_one_left (apply_nonneg p _) ha
_ < r := by rwa [mem_ball_zero] at hy
