rw [mem_combiFrontier_iff] at hy
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x y : E
hy : y ∈ combiFrontier 𝕜 {x}
⊢ y ∈ ∅
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x y : E
hy : ∃ t ⊂ {x}, y ∈ (convexHull 𝕜) ↑t
⊢ y ∈ ∅