no goals
α : Type u
β : Type v
X : Type ?u.491428
ι : Type ?u.491431
inst✝ : PseudoMetricSpace α
x : α
s t : Set α
r : ℝ
⊢ Bounded (s ∪ t) ↔ Bounded s ∧ Bounded t
simp only [bounded_iff_isBounded, isBounded_union]