exact hs _ hxs (convex_iff_openSegment_subset.1 (convex_convexHull 𝕜 _) h.1 h.2 hx.1)
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
x₁ : E
hx₁ : x₁ ∈ (convexHull 𝕜) s
x₂ : E
hx₂ : x₂ ∈ (convexHull 𝕜) s
hx : x ∈ openSegment 𝕜 x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
h : x₁ ∈ (convexHull 𝕜) (s \ {x}) ∧ x₂ ∈ (convexHull 𝕜) (s \ {x})
⊢ False
no goals