no goals
𝕜 : Type u_2
𝕜' : Type ?u.254043
E : Type u_1
E' : Type ?u.254049
F : Type ?u.254052
ι : Type ?u.254055
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ ∃ r, ∀ (x : E), x ∈ s → ‖x‖ ≤ r
rw [NormedSpace.isVonNBounded_iff, ← Metric.bounded_iff_isBounded, bounded_iff_forall_norm_le]