case inl
ι : Sort ?u.107462
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
hδ : δ < 0
⊢ closedBall x δ ⊆ cthickening δ {x}

case inr
ι : Sort ?u.107462
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
hδ : 0 ≤ δ
⊢ closedBall x δ ⊆ cthickening δ {x}
ι : Sort ?u.107462
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
⊢ closedBall x δ ⊆ cthickening δ {x}
rcases lt_or_le δ 0 with (hδ | hδ)
no goals
case inl
ι : Sort ?u.107462
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
hδ : δ < 0
⊢ closedBall x δ ⊆ cthickening δ {x}
simp only [closedBall_eq_empty.mpr hδ, empty_subset]
no goals
case inr
ι : Sort ?u.107462
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
hδ : 0 ≤ δ
⊢ closedBall x δ ⊆ cthickening δ {x}
simp only [cthickening_singleton x hδ, Subset.rfl]