no goals
𝕜 : Type u_2
𝕜' : Type ?u.256544
E : Type u_3
E' : Type u_1
F : Type ?u.256553
ι : Type ?u.256556
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E' → E
s : Set E'
⊢ Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∃ r, ∀ (x : E'), x ∈ s → ‖f x‖ ≤ r
simp_rw [isVonNBounded_iff', Set.ball_image_iff]