R : Type ?u.1453031
R' : Type ?u.1453034
𝕜 : Type u_1
𝕜₂ : Type ?u.1453040
𝕜₃ : Type ?u.1453043
𝕝 : Type ?u.1453046
E : Type u_2
E₂ : Type ?u.1453052
E₃ : Type ?u.1453055
F : Type ?u.1453058
G : Type ?u.1453061
ι : Type ?u.1453064
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
x : E
hr : 0 < r
⊢ Absorbent 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) 0 r)
R : Type ?u.1453031
R' : Type ?u.1453034
𝕜 : Type u_1
𝕜₂ : Type ?u.1453040
𝕜₃ : Type ?u.1453043
𝕝 : Type ?u.1453046
E : Type u_2
E₂ : Type ?u.1453052
E₃ : Type ?u.1453055
F : Type ?u.1453058
G : Type ?u.1453061
ι : Type ?u.1453064
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
x : E
hr : 0 < r
⊢ Absorbent 𝕜 (Metric.ball 0 r)
rw [← ball_normSeminorm 𝕜]
no goals
R : Type ?u.1453031
R' : Type ?u.1453034
𝕜 : Type u_1
𝕜₂ : Type ?u.1453040
𝕜₃ : Type ?u.1453043
𝕝 : Type ?u.1453046
E : Type u_2
E₂ : Type ?u.1453052
E₃ : Type ?u.1453055
F : Type ?u.1453058
G : Type ?u.1453061
ι : Type ?u.1453064
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
x : E
hr : 0 < r
⊢ Absorbent 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) 0 r)
exact (normSeminorm _ _).absorbent_ball_zero hr