no goals
ι : Sort ?u.113978
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t✝ : Set α
x : α
δ : ℝ
s t : Set α
⊢ thickening δ (s ∪ t) = thickening δ s ∪ thickening δ t
simp_rw [thickening, infEdist_union, inf_eq_min, min_lt_iff, setOf_or]