rw [Convex.convexHull_eq hA₁, inter_eq_self_of_subset_right frontier_subset_closure]
case h.e'_7
𝕜 : 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
⊢ frontier s = closure s ∩ frontier ((convexHull 𝕜) s)
no goals