case inl
ι : Type ?u.29650
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
hs : Convex ℝ s
δ : ℝ
hδ : 0 ≤ δ
⊢ Convex ℝ (Metric.cthickening δ s)

case inr
ι : Type ?u.29650
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
hs : Convex ℝ s
δ : ℝ
hδ : δ ≤ 0
⊢ Convex ℝ (Metric.cthickening δ s)
ι : Type ?u.29650
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
hs : Convex ℝ s
δ : ℝ
⊢ Convex ℝ (Metric.cthickening δ s)
obtain hδ | hδ := le_total 0 δ
case inl
ι : Type ?u.29650
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
hs : Convex ℝ s
δ : ℝ
hδ : 0 ≤ δ
⊢ Convex ℝ (⋂ (ε : ℝ) (_ : δ < ε), Metric.thickening ε s)
case inl
ι : Type ?u.29650
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
hs : Convex ℝ s
δ : ℝ
hδ : 0 ≤ δ
⊢ Convex ℝ (Metric.cthickening δ s)
rw [cthickening_eq_iInter_thickening hδ]
no goals
case inl
ι : Type ?u.29650
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
hs : Convex ℝ s
δ : ℝ
hδ : 0 ≤ δ
⊢ Convex ℝ (⋂ (ε : ℝ) (_ : δ < ε), Metric.thickening ε s)
exact convex_iInter₂ fun _ _ => hs.thickening _
case inr
ι : Type ?u.29650
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
hs : Convex ℝ s
δ : ℝ
hδ : δ ≤ 0
⊢ Convex ℝ (closure s)
case inr
ι : Type ?u.29650
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
hs : Convex ℝ s
δ : ℝ
hδ : δ ≤ 0
⊢ Convex ℝ (Metric.cthickening δ s)
rw [cthickening_of_nonpos hδ]
no goals
case inr
ι : Type ?u.29650
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
hs : Convex ℝ s
δ : ℝ
hδ : δ ≤ 0
⊢ Convex ℝ (closure s)
exact hs.closure