R : Type ?u.826028
R' : Type ?u.826031
𝕜 : Type u_2
𝕜₂ : Type ?u.826037
𝕜₃ : Type ?u.826040
𝕝 : Type ?u.826043
E : Type u_1
E₂ : Type ?u.826049
E₃ : Type ?u.826052
F : Type ?u.826055
G : Type ?u.826058
ι : Type ?u.826061
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x✝ y : E
r : ℝ
x : E
hr : 0 < r
⊢ ∀ (x_1 : E), x_1 ∈ {y | ↑0 (y - x) < r}
R : Type ?u.826028
R' : Type ?u.826031
𝕜 : Type u_2
𝕜₂ : Type ?u.826037
𝕜₃ : Type ?u.826040
𝕝 : Type ?u.826043
E : Type u_1
E₂ : Type ?u.826049
E₃ : Type ?u.826052
F : Type ?u.826055
G : Type ?u.826058
ι : Type ?u.826061
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x✝ y : E
r : ℝ
x : E
hr : 0 < r
⊢ ball 0 x r = univ
rw [Set.eq_univ_iff_forall, ball]
no goals
R : Type ?u.826028
R' : Type ?u.826031
𝕜 : Type u_2
𝕜₂ : Type ?u.826037
𝕜₃ : Type ?u.826040
𝕝 : Type ?u.826043
E : Type u_1
E₂ : Type ?u.826049
E₃ : Type ?u.826052
F : Type ?u.826055
G : Type ?u.826058
ι : Type ?u.826061
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x✝ y : E
r : ℝ
x : E
hr : 0 < r
⊢ ∀ (x_1 : E), x_1 ∈ {y | ↑0 (y - x) < r}
simp [hr]