no goals
α✝ : Type ?u.106997
β✝ : Type ?u.107000
ι : Type ?u.107003
π : ι → Type ?u.107008
inst✝⁴ : Fintype ι
inst✝³ : Bornology α✝
inst✝² : Bornology β✝
inst✝¹ : (i : ι) → Bornology (π i)
α : Type u_1
β : Type u_2
inst✝ : Bornology β
f : α → β
⊢ BoundedSpace α ↔ IsBounded (range f)
rw [← @isBounded_univ _ (Bornology.induced f), isBounded_induced, image_univ]