no goals
α : Type u
β : Type v
X : Type ?u.491823
ι : Type ?u.491826
inst✝ : PseudoMetricSpace α
x : α
s✝ t : Set α
r : ℝ
I : Set β
s : β → Set α
H : Set.Finite I
⊢ Bounded (⋃ (i : β) (_ : i ∈ I), s i) ↔ ∀ (i : β), i ∈ I → Bounded (s i)
simp only [bounded_iff_isBounded, isBounded_biUnion H]