no goals
ι : Sort ?u.102452
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
E : Set α
⊢ cthickening (max 0 δ) E = cthickening δ E
cases le_total δ 0 <;> simp [cthickening_of_nonpos, *]