Theorem: Geometry.SimplicialComplex.simplex_combiInteriors_split_interiors (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 : ℕ
ht : AffineIndependent 𝕜 Subtype.val
hst : (convexHull 𝕜) ↑s ⊆ (convexHull 𝕜) ↑t
⊢ ∃ u ⊆ t, combiInterior 𝕜 s ⊆ combiInterior 𝕜 u
Tactic:
classical
let K := SimplicialComplex.ofSimplex ht
let F := t.powerset.filter fun v : Finset E => (s : Set E) ⊆ convexHull 𝕜 ↑v
sorry
State after:
no goals

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 : ℕ
ht : AffineIndependent 𝕜 Subtype.val
hst : (convexHull 𝕜) ↑s ⊆ (convexHull 𝕜) ↑t
⊢ ∃ u ⊆ t, combiInterior 𝕜 s ⊆ combiInterior 𝕜 u
Tactic:
let K := SimplicialComplex.ofSimplex ht
State after:
𝕜 : 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
⊢ ∃ u ⊆ t, combiInterior 𝕜 s ⊆ combiInterior 𝕜 u

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 : ℕ
ht : AffineIndependent 𝕜 Subtype.val
hst : (convexHull 𝕜) ↑s ⊆ (convexHull 𝕜) ↑t
K : SimplicialComplex 𝕜 E := ofSimplex ht
⊢ ∃ u ⊆ t, combiInterior 𝕜 s ⊆ combiInterior 𝕜 u
Tactic:
let F := t.powerset.filter fun v : Finset E => (s : Set E) ⊆ convexHull 𝕜 ↑v
State after:
𝕜 : 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

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 : ℕ
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
Tactic:
sorry
State after:
no goals