𝕜 : Type u_1
𝕜' : Type ?u.235860
E : Type u_2
E' : Type ?u.235866
F : Type ?u.235869
ι : Type ?u.235872
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ ∀ (i : ℝ), 0 < i → Absorbs 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) 0 i) (Seminorm.ball (normSeminorm 𝕜 E) 0 r)
𝕜 : Type u_1
𝕜' : Type ?u.235860
E : Type u_2
E' : Type ?u.235866
F : Type ?u.235869
ι : Type ?u.235872
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ Bornology.IsVonNBounded 𝕜 (Metric.ball 0 r)
rw [Metric.nhds_basis_ball.isVonNBounded_basis_iff, ← ball_normSeminorm 𝕜 E]
no goals
𝕜 : Type u_1
𝕜' : Type ?u.235860
E : Type u_2
E' : Type ?u.235866
F : Type ?u.235869
ι : Type ?u.235872
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ ∀ (i : ℝ), 0 < i → Absorbs 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) 0 i) (Seminorm.ball (normSeminorm 𝕜 E) 0 r)
exact fun ε hε => (normSeminorm 𝕜 E).ball_zero_absorbs_ball_zero hε