Theorem: Geometry.SimplicialComplex.mem_combiFrontier_iff' (LeanCamCombi/SimplicialComplex/Basic.lean)

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ x ∈ combiFrontier 𝕜 s ↔ ∃ t ⊂ s, x ∈ combiInterior 𝕜 t
Tactic:
rw [mem_combiFrontier_iff]
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ (∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t) ↔ ∃ t ⊂ s, x ∈ combiInterior 𝕜 t

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ (∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t) ↔ ∃ t ⊂ s, x ∈ combiInterior 𝕜 t
Tactic:
constructor
State after:
case mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ (∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t) → ∃ t ⊂ s, x ∈ combiInterior 𝕜 t

case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ (∃ t ⊂ s, x ∈ combiInterior 𝕜 t) → ∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t

State before:
case mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ (∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t) → ∃ t ⊂ s, x ∈ combiInterior 𝕜 t
Tactic:
rintro ⟨t, hts, hxt⟩
State after:
case mp.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t✝ : Finset E
A : Set (Finset E)
m n : ℕ
t : Finset E
hts : t ⊂ s
hxt : x ∈ (convexHull 𝕜) ↑t
⊢ ∃ t ⊂ s, x ∈ combiInterior 𝕜 t

State before:
case mp.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t✝ : Finset E
A : Set (Finset E)
m n : ℕ
t : Finset E
hts : t ⊂ s
hxt : x ∈ (convexHull 𝕜) ↑t
⊢ ∃ t ⊂ s, x ∈ combiInterior 𝕜 t
Tactic:
sorry
State after:
no goals

State before:
case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ (∃ t ⊂ s, x ∈ combiInterior 𝕜 t) → ∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t
Tactic:
rintro ⟨t, hts, hxt⟩
State after:
case mpr.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t✝ : Finset E
A : Set (Finset E)
m n : ℕ
t : Finset E
hts : t ⊂ s
hxt : x ∈ combiInterior 𝕜 t
⊢ ∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t

State before:
case mpr.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t✝ : Finset E
A : Set (Finset E)
m n : ℕ
t : Finset E
hts : t ⊂ s
hxt : x ∈ combiInterior 𝕜 t
⊢ ∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t
Tactic:
exact ⟨t, hts, hxt.1⟩
State after:
no goals