𝓕 : Type ?u.128861
𝕜 : Type ?u.128864
α : Type ?u.128867
ι : Type ?u.128870
κ : Type ?u.128873
E : Type u_1
F : Type ?u.128879
G : Type ?u.128882
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
x : E
⊢ HasBasis (𝓝 x) (fun ε => 0 < ε) fun ε => ball x ε
𝓕 : Type ?u.128861
𝕜 : Type ?u.128864
α : Type ?u.128867
ι : Type ?u.128870
κ : Type ?u.128873
E : Type u_1
F : Type ?u.128879
G : Type ?u.128882
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
x : E
⊢ HasBasis (𝓝 x) (fun ε => 0 < ε) fun ε => {y | ‖y / x‖ < ε}
simp_rw [← ball_eq']
no goals
𝓕 : Type ?u.128861
𝕜 : Type ?u.128864
α : Type ?u.128867
ι : Type ?u.128870
κ : Type ?u.128873
E : Type u_1
F : Type ?u.128879
G : Type ?u.128882
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
x : E
⊢ HasBasis (𝓝 x) (fun ε => 0 < ε) fun ε => ball x ε
exact Metric.nhds_basis_ball