sorry
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K✝ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
ht : AffineIndependent 𝕜 Subtype.val
hst : (convexHull 𝕜) ↑s ⊆ (convexHull 𝕜) ↑t
K : SimplicialComplex 𝕜 E := ofSimplex ht
F : Finset (Finset E) := filter (fun v => ↑s ⊆ (convexHull 𝕜) ↑v) t.powerset
⊢ ∃ u ⊆ t, combiInterior 𝕜 s ⊆ combiInterior 𝕜 u
no goals