Theorem: Geometry.SimplicialComplex.simplex_combiInteriors_split_interiors_nonempty (LeanCamCombi/SimplicialComplex/Basic.lean)

State before:
𝕜 : 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 : ℕ
hs : s.Nonempty
ht : AffineIndependent 𝕜 Subtype.val
hst : (convexHull 𝕜) ↑s ⊆ (convexHull 𝕜) ↑t
⊢ ∃ u ⊆ t, u.Nonempty ∧ combiInterior 𝕜 s ⊆ combiInterior 𝕜 u
Tactic:
sorry
State after:
no goals