R : Type ?u.1455685
R' : Type ?u.1455688
𝕜 : Type u_2
𝕜₂ : Type ?u.1455694
𝕜₃ : Type ?u.1455697
𝕝 : Type ?u.1455700
E : Type u_1
E₂ : Type ?u.1455706
E₃ : Type ?u.1455709
F : Type ?u.1455712
G : Type ?u.1455715
ι : Type ?u.1455718
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
x : E
hx : ‖x‖ < r
⊢ Absorbent 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) x r)
R : Type ?u.1455685
R' : Type ?u.1455688
𝕜 : Type u_2
𝕜₂ : Type ?u.1455694
𝕜₃ : Type ?u.1455697
𝕝 : Type ?u.1455700
E : Type u_1
E₂ : Type ?u.1455706
E₃ : Type ?u.1455709
F : Type ?u.1455712
G : Type ?u.1455715
ι : Type ?u.1455718
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
x : E
hx : ‖x‖ < r
⊢ Absorbent 𝕜 (Metric.ball x r)
rw [← ball_normSeminorm 𝕜]
no goals
R : Type ?u.1455685
R' : Type ?u.1455688
𝕜 : Type u_2
𝕜₂ : Type ?u.1455694
𝕜₃ : Type ?u.1455697
𝕝 : Type ?u.1455700
E : Type u_1
E₂ : Type ?u.1455706
E₃ : Type ?u.1455709
F : Type ?u.1455712
G : Type ?u.1455715
ι : Type ?u.1455718
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
x : E
hx : ‖x‖ < r
⊢ Absorbent 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) x r)
exact (normSeminorm _ _).absorbent_ball hx