case δ_nn
ι : Sort ?u.143302
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
E : Set α
⊢ 0 ≤ max 0 δ
ι : Sort ?u.143302
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
E : Set α
⊢ cthickening δ E = ⋂ (ε : ℝ) (_ : max 0 δ < ε), thickening ε E
rw [← cthickening_max_zero, cthickening_eq_iInter_thickening]
no goals
case δ_nn
ι : Sort ?u.143302
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
E : Set α
⊢ 0 ≤ max 0 δ
exact le_max_left _ _