no goals
ι : Type u_1
α : Type u_2
β : Type ?u.7851
s✝ : Set α
inst✝ : Bornology α
s : Set ι
f : ι → Set α
hs : Set.Finite s
⊢ IsBounded (⋃ (i : ι) (_ : i ∈ s), f i) ↔ ∀ (i : ι), i ∈ s → IsBounded (f i)
simp only [← isCobounded_compl_iff, compl_iUnion, isCobounded_biInter hs]