exact (IsClosed.closure_eq hA₂).symm
case h.e'_6
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hA₁ : Convex 𝕜 s
hA₂ : IsClosed s
⊢ s = closure s
no goals