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

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
⊢ combiFrontier ℝ s = frontier ((convexHull ℝ) ↑s)
Tactic:
ext x
State after:
case h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
⊢ x ∈ combiFrontier ℝ s ↔ x ∈ frontier ((convexHull ℝ) ↑s)

State before:
case h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
⊢ x ∈ combiFrontier ℝ s ↔ x ∈ frontier ((convexHull ℝ) ↑s)
Tactic:
constructor
State after:
case h.mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
⊢ x ∈ combiFrontier ℝ s → x ∈ frontier ((convexHull ℝ) ↑s)

case h.mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
⊢ x ∈ frontier ((convexHull ℝ) ↑s) → x ∈ combiFrontier ℝ s

State before:
case h.mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
⊢ x ∈ combiFrontier ℝ s → x ∈ frontier ((convexHull ℝ) ↑s)
Tactic:
unfold combiFrontier
State after:
case h.mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊂ s), (convexHull ℝ) ↑t → x ∈ frontier ((convexHull ℝ) ↑s)

State before:
case h.mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊂ s), (convexHull ℝ) ↑t → x ∈ frontier ((convexHull ℝ) ↑s)
Tactic:
simp_rw [Set.mem_iUnion]
State after:
case h.mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
⊢ (∃ i, ∃ (_ : i ⊂ s), x ∈ (convexHull ℝ) ↑i) → x ∈ frontier ((convexHull ℝ) ↑s)

State before:
case h.mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
⊢ (∃ i, ∃ (_ : i ⊂ s), x ∈ (convexHull ℝ) ↑i) → x ∈ frontier ((convexHull ℝ) ↑s)
Tactic:
rintro ⟨t, hts, hx⟩
State after:
case h.mp.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t✝ : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
t : Finset E
hts : t ⊂ s
hx : x ∈ (convexHull ℝ) ↑t
⊢ x ∈ frontier ((convexHull ℝ) ↑s)

State before:
case h.mp.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t✝ : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
t : Finset E
hts : t ⊂ s
hx : x ∈ (convexHull ℝ) ↑t
⊢ x ∈ frontier ((convexHull ℝ) ↑s)
Tactic:
constructor
State after:
case h.mp.intro.intro.left
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t✝ : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
t : Finset E
hts : t ⊂ s
hx : x ∈ (convexHull ℝ) ↑t
⊢ x ∈ closure ((convexHull ℝ) ↑s)

case h.mp.intro.intro.right
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t✝ : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
t : Finset E
hts : t ⊂ s
hx : x ∈ (convexHull ℝ) ↑t
⊢ x ∉ interior ((convexHull ℝ) ↑s)

State before:
case h.mp.intro.intro.left
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t✝ : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
t : Finset E
hts : t ⊂ s
hx : x ∈ (convexHull ℝ) ↑t
⊢ x ∈ closure ((convexHull ℝ) ↑s)
Tactic:
exact subset_closure (convexHull_mono hts.1 hx)
State after:
no goals

State before:
case h.mp.intro.intro.right
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t✝ : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
t : Finset E
hts : t ⊂ s
hx : x ∈ (convexHull ℝ) ↑t
⊢ x ∉ interior ((convexHull ℝ) ↑s)
Tactic:
rintro h
State after:
case h.mp.intro.intro.right
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t✝ : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
t : Finset E
hts : t ⊂ s
hx : x ∈ (convexHull ℝ) ↑t
h : x ∈ interior ((convexHull ℝ) ↑s)
⊢ False

State before:
case h.mp.intro.intro.right
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t✝ : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
t : Finset E
hts : t ⊂ s
hx : x ∈ (convexHull ℝ) ↑t
h : x ∈ interior ((convexHull ℝ) ↑s)
⊢ False
Tactic:
sorry
State after:
no goals

State before:
case h.mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
⊢ x ∈ frontier ((convexHull ℝ) ↑s) → x ∈ combiFrontier ℝ s
Tactic:
rintro ⟨h, g⟩
State after:
case h.mpr.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
h : x ∈ closure ((convexHull ℝ) ↑s)
g : x ∉ interior ((convexHull ℝ) ↑s)
⊢ x ∈ combiFrontier ℝ s

State before:
case h.mpr.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
h : x ∈ closure ((convexHull ℝ) ↑s)
g : x ∉ interior ((convexHull ℝ) ↑s)
⊢ x ∈ combiFrontier ℝ s
Tactic:
sorry
State after:
no goals