no goals
ι : Type u_1
α : Type u_2
β : Type ?u.8981
s✝ : Set α
inst✝¹ : Bornology α
inst✝ : Finite ι
s : ι → Set α
⊢ IsBounded (⋃ (i : ι), s i) ↔ ∀ (i : ι), IsBounded (s i)
rw [← sUnion_range, isBounded_sUnion (finite_range s), forall_range_iff]