no goals
ι : Sort ?u.100122
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
⊢ cthickening δ ∅ = ∅
simp only [cthickening, ENNReal.ofReal_ne_top, setOf_false, infEdist_empty, top_le_iff]