no goals
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
f : ι → Set α
⊢ thickening δ (⋃ (i : ι), f i) = ⋃ (i : ι), thickening δ (f i)
simp_rw [thickening, infEdist_iUnion, iInf_lt_iff, setOf_exists]