balanced_closedBall_zero — Mathlib

English

Let p : ι → Seminorm 𝕜 E; S finite; x ∈ E; r ≥ 0. Then closedBall(sup p) x r = ⋂ i ∈ S, closedBall(p i) x r.

Русский

Пусть p : ι → Seminorm 𝕜 E; S конечен; x ∈ E; r ≥ 0. Тогда closedBall(sup p) x r = ⋂ i ∈ S, closedBall(p i) x r.

LaTeX

$$$\text{closedBall}(\,s.\sup p\,)\,x\,r = \bigcap_{i \in s} \text{closedBall}(p i)\,x\,r$$$

Lean4

/-- Closed seminorm-balls at the origin are balanced. -/
theorem balanced_closedBall_zero (r : ℝ) : Balanced 𝕜 (closedBall p 0 r) :=
  by
  rintro a ha x ⟨y, hy, hx⟩
  rw [mem_closedBall_zero, ← hx, map_smul_eq_mul]
  calc
    _ ≤ p y := mul_le_of_le_one_left (apply_nonneg p _) ha
    _ ≤ r := by rwa [mem_closedBall_zero] at hy

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