no goals
R : Type ?u.792081
R' : Type ?u.792084
𝕜 : Type u_2
𝕜₂ : Type ?u.792090
𝕜₃ : Type ?u.792093
𝕝 : Type ?u.792096
E : Type u_1
E₂ : Type ?u.792102
E₃ : Type ?u.792105
F : Type ?u.792108
G : Type ?u.792111
ι : Type ?u.792114
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x y : E
r : ℝ
hr : 0 < r
⊢ x ∈ ball p x r
simp [hr]