no goals
R : Type ?u.817019
R' : Type ?u.817022
𝕜 : Type u_2
𝕜₂ : Type ?u.817028
𝕜₃ : Type ?u.817031
𝕝 : Type ?u.817034
E : Type u_1
E₂ : Type ?u.817040
E₃ : Type ?u.817043
F : Type ?u.817046
G : Type ?u.817049
ι : Type ?u.817052
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x y : E
r : ℝ
⊢ y ∈ ball p 0 r ↔ ↑p y < r
rw [mem_ball, sub_zero]