no goals
ι : Type ?u.8797
α : Type u_1
β : Type ?u.8803
s : Set α
inst✝ : Bornology α
S : Set (Set α)
hs : Set.Finite S
⊢ IsBounded (⋃₀ S) ↔ ∀ (s : Set α), s ∈ S → IsBounded s
rw [sUnion_eq_biUnion, isBounded_biUnion hs]