R : Type ?u.1457964
R' : Type ?u.1457967
𝕜 : Type u_1
𝕜₂ : Type ?u.1457973
𝕜₃ : Type ?u.1457976
𝕝 : Type ?u.1457979
E : Type u_2
E₂ : Type ?u.1457985
E₃ : Type ?u.1457988
F : Type ?u.1457991
G : Type ?u.1457994
ι : Type ?u.1457997
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
x : E
⊢ Balanced 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) 0 r)
R : Type ?u.1457964
R' : Type ?u.1457967
𝕜 : Type u_1
𝕜₂ : Type ?u.1457973
𝕜₃ : Type ?u.1457976
𝕝 : Type ?u.1457979
E : Type u_2
E₂ : Type ?u.1457985
E₃ : Type ?u.1457988
F : Type ?u.1457991
G : Type ?u.1457994
ι : Type ?u.1457997
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
x : E
⊢ Balanced 𝕜 (Metric.ball 0 r)
rw [← ball_normSeminorm 𝕜]
no goals
R : Type ?u.1457964
R' : Type ?u.1457967
𝕜 : Type u_1
𝕜₂ : Type ?u.1457973
𝕜₃ : Type ?u.1457976
𝕝 : Type ?u.1457979
E : Type u_2
E₂ : Type ?u.1457985
E₃ : Type ?u.1457988
F : Type ?u.1457991
G : Type ?u.1457994
ι : Type ?u.1457997
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
x : E
⊢ Balanced 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) 0 r)
exact (normSeminorm _ _).balanced_ball_zero r