𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
⊢ Set.Nonempty (↑(convexHull 𝕜).toOrderHom ↑(minCardFinsetOfMemConvexHull hx))
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
⊢ Finset.Nonempty (minCardFinsetOfMemConvexHull hx)
rw [← Finset.coe_nonempty, ← @convexHull_nonempty_iff 𝕜]
no goals
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
⊢ Set.Nonempty (↑(convexHull 𝕜).toOrderHom ↑(minCardFinsetOfMemConvexHull hx))
exact ⟨x, mem_minCardFinsetOfMemConvexHull hx⟩