ι : Sort ?u.145496
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
E : Set α
⊢ cthickening 0 E = ⋂ (δ : ℝ) (_ : 0 < δ), thickening δ E
ι : Sort ?u.145496
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
E : Set α
⊢ closure E = ⋂ (δ : ℝ) (_ : 0 < δ), thickening δ E
rw [← cthickening_zero]
no goals
ι : Sort ?u.145496
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
E : Set α
⊢ cthickening 0 E = ⋂ (δ : ℝ) (_ : 0 < δ), thickening δ E
exact cthickening_eq_iInter_thickening rfl.ge E