no goals
R : Type ?u.804396
R' : Type ?u.804399
𝕜 : Type u_2
𝕜₂ : Type ?u.804405
𝕜₃ : Type ?u.804408
𝕝 : Type ?u.804411
E : Type u_1
E₂ : Type ?u.804417
E₃ : Type ?u.804420
F : Type ?u.804423
G : Type ?u.804426
ι : Type ?u.804429
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x y : E
r : ℝ
hr : 0 ≤ r
⊢ x ∈ closedBall p x r
simp [hr]