no goals
R : Type ?u.818815
R' : Type ?u.818818
𝕜 : Type u_2
𝕜₂ : Type ?u.818824
𝕜₃ : Type ?u.818827
𝕝 : Type ?u.818830
E : Type u_1
E₂ : Type ?u.818836
E₃ : Type ?u.818839
F : Type ?u.818842
G : Type ?u.818845
ι : Type ?u.818848
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x y : E
r : ℝ
⊢ y ∈ closedBall p 0 r ↔ ↑p y ≤ r
rw [mem_closedBall, sub_zero]