no goals
𝕜 : Type u_2
𝕜₂ : Type ?u.493266
𝕝 : Type ?u.493269
𝕝₂ : Type ?u.493272
E : Type u_3
F : Type ?u.493278
G : Type u_1
ι : Type u_4
ι' : Type ?u.493287
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
f : G → E
s : Set G
hp : WithSeminorms p
⊢ Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∀ (i : ι), ∃ r, r > 0 ∧ ∀ (x : G), x ∈ s → ↑(p i) (f x) < r
simp_rw [hp.isVonNBounded_iff_seminorm_bounded, Set.ball_image_iff]