sorry
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ x₁ : E
hx₁A : x₁ ∈ closure s
x₂ : E
hx₂A : x₂ ∈ closure s
x : E
hxs : x ∈ closure s ∩ frontier ((convexHull 𝕜) s)
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₂ ∈ frontier ((convexHull 𝕜) s)
no goals