ι : Sort ?u.146423
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
x : α
E : Set α
hx : x ∈ E
δ : ℝ
⊢ {x} ⊆ E
ι : Sort ?u.146423
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
x : α
E : Set α
hx : x ∈ E
δ : ℝ
⊢ closedBall x δ ⊆ cthickening δ E
refine' (closedBall_subset_cthickening_singleton _ _).trans (cthickening_subset_of_subset _ _)
no goals
ι : Sort ?u.146423
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
x : α
E : Set α
hx : x ∈ E
δ : ℝ
⊢ {x} ⊆ E
simpa using hx