α : Type u_1
ι : Type ?u.1091
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (⋂ (ε_1 : ℝ) (_ : max 0 ε < ε_1), thickening ε_1 s)
α : Type u_1
ι : Type ?u.1091
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (cthickening ε s)
rw [cthickening_eq_iInter_thickening'']
no goals
α : Type u_1
ι : Type ?u.1091
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (⋂ (ε_1 : ℝ) (_ : max 0 ε < ε_1), thickening ε_1 s)
exact isUpperSet_iInter₂ fun δ _ => hs.thickening' _