Theorem: mem_combiFrontier_iff (LeanCamCombi/SimplicialComplex/Simplex.lean)

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ x ∈ combiFrontier 𝕜 s ↔ ∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t
Tactic:
simp [combiFrontier]
State after:
no goals