no goals
ι : Type ?u.4828
α : Type u_1
β : Type ?u.4834
inst✝ : Bornology α
s t : Set α
x : α
⊢ IsBounded (s ∪ t) ↔ IsBounded s ∧ IsBounded t
simp only [← isCobounded_compl_iff, compl_union, isCobounded_inter]