case h.h.h
R : Type ?u.1449022
R' : Type ?u.1449025
𝕜 : Type u_2
𝕜₂ : Type ?u.1449031
𝕜₃ : Type ?u.1449034
𝕝 : Type ?u.1449037
E : Type u_1
E₂ : Type ?u.1449043
E₃ : Type ?u.1449046
F : Type ?u.1449049
G : Type ?u.1449052
ι : Type ?u.1449055
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r✝ : ℝ
x : E
r : ℝ
y : E
⊢ y ∈ Seminorm.ball (normSeminorm 𝕜 E) x r ↔ y ∈ Metric.ball x r
R : Type ?u.1449022
R' : Type ?u.1449025
𝕜 : Type u_2
𝕜₂ : Type ?u.1449031
𝕜₃ : Type ?u.1449034
𝕝 : Type ?u.1449037
E : Type u_1
E₂ : Type ?u.1449043
E₃ : Type ?u.1449046
F : Type ?u.1449049
G : Type ?u.1449052
ι : Type ?u.1449055
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ Seminorm.ball (normSeminorm 𝕜 E) = Metric.ball
ext (x r y)
no goals
case h.h.h
R : Type ?u.1449022
R' : Type ?u.1449025
𝕜 : Type u_2
𝕜₂ : Type ?u.1449031
𝕜₃ : Type ?u.1449034
𝕝 : Type ?u.1449037
E : Type u_1
E₂ : Type ?u.1449043
E₃ : Type ?u.1449046
F : Type ?u.1449049
G : Type ?u.1449052
ι : Type ?u.1449055
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r✝ : ℝ
x : E
r : ℝ
y : E
⊢ y ∈ Seminorm.ball (normSeminorm 𝕜 E) x r ↔ y ∈ Metric.ball x r
simp only [Seminorm.mem_ball, Metric.mem_ball, coe_normSeminorm, dist_eq_norm]