no goals
α : Type u_1
β : Type ?u.107189
ι : Type ?u.107192
π : ι → Type ?u.107197
inst✝³ : Fintype ι
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : (i : ι) → Bornology (π i)
p : α → Prop
⊢ BoundedSpace (Subtype p) ↔ IsBounded {x | p x}
rw [boundedSpace_induced_iff, Subtype.range_coe_subtype]