internlm/Lean-Github huggingface dataset:
Theorem: convex_combiInterior
Proof state before:
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
⊢ a • s.centerMass v id + b • s.centerMass w id ∈
    {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}
Tactic:
refine' ⟨fun x => a * v x + b * w x, fun x hx => _, _, _⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ : E
hs : AffineIndependent 𝕜 Subtype.val
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
x : E
hx : x ∈ s
⊢ 0 < (fun x => a * v x + b * w x) x

case intro.intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
⊢ ∑ y ∈ s, (fun x => a * v x + b * w x) y = 1

case intro.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
⊢ s.centerMass (fun x => a * v x + b * w x) id = a • s.centerMass v id + b • s.centerMass w id
Theorem: convex_combiInterior
Proof state before:
case intro.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
⊢ s.centerMass (fun x => a * v x + b * w x) id = a • s.centerMass v id + b • s.centerMass w id
Tactic:
rw [Finset.centerMass_segment _ _ _ _ hv₁ hw₁ _ _ h]
Proof state after:
no goals
Theorem: convex_combiInterior
Proof state before:
case intro.intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ : E
hs : AffineIndependent 𝕜 Subtype.val
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
x : E
hx : x ∈ s
⊢ 0 < (fun x => a * v x + b * w x) x
Tactic:
exact add_pos (mul_pos ha <| hv₀ x hx) (mul_pos hb <| hw₀ x hx)
Proof state after:
no goals
Theorem: convex_combiInterior
Proof state before:
case intro.intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
⊢ ∑ y ∈ s, (fun x => a * v x + b * w x) y = 1
Tactic:
rw [Finset.sum_add_distrib, ← Finset.mul_sum, ← Finset.mul_sum, hv₁, hw₁]
Proof state after:
case intro.intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
⊢ a * 1 + b * 1 = 1
Theorem: convex_combiInterior
Proof state before:
case intro.intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
⊢ a * 1 + b * 1 = 1
Tactic:
simp [h]
Proof state after:
no goals
Theorem: isClosed_combiFrontier
Proof 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
⊢ IsClosed (combiFrontier ℝ s)
Tactic:
refine' Set.Finite.isClosed_biUnion _ fun t _ => t.isClosed_convexHull
Proof state after:
𝕜 : 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
⊢ Set.Finite fun t => t ⊆ s ∧ ¬s ⊆ t
Theorem: isClosed_combiFrontier
Proof 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
⊢ Set.Finite fun t => t ⊆ s ∧ ¬s ⊆ t
Tactic:
suffices Set.Finite {t | t ⊆ s} by exact this.subset fun i h => h.1
Proof state after:
𝕜 : 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
⊢ {t | t ⊆ s}.Finite
Theorem: isClosed_combiFrontier
Proof 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
⊢ {t | t ⊆ s}.Finite
Tactic:
convert s.powerset.finite_toSet using 1
Proof state after:
case h.e'_2
𝕜 : 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
⊢ {t | t ⊆ s} = ↑s.powerset
Theorem: isClosed_combiFrontier
Proof state before:
case h.e'_2
𝕜 : 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
⊢ {t | t ⊆ s} = ↑s.powerset
Tactic:
ext
Proof state after:
case h.e'_2.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 x✝ : Finset E
⊢ x✝ ∈ {t | t ⊆ s} ↔ x✝ ∈ ↑s.powerset
Theorem: isClosed_combiFrontier
Proof state before:
case h.e'_2.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 x✝ : Finset E
⊢ x✝ ∈ {t | t ⊆ s} ↔ x✝ ∈ ↑s.powerset
Tactic:
simp
Proof state after:
no goals
Theorem: isClosed_combiFrontier
Proof 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
this : {t | t ⊆ s}.Finite
⊢ Set.Finite fun t => t ⊆ s ∧ ¬s ⊆ t
Tactic:
exact this.subset fun i h => h.1
Proof state after:
no goals
Theorem: interiors_agree_of_full_dimensional
Proof 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
hs : AffineIndependent ℝ Subtype.val
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
⊢ combiInterior ℝ s = interior ((convexHull ℝ) ↑s)
Tactic:
unfold combiInterior
Proof state after:
𝕜 : 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
hs : AffineIndependent ℝ Subtype.val
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
⊢ (convexHull ℝ) ↑s \ combiFrontier ℝ s = interior ((convexHull ℝ) ↑s)
Theorem: interiors_agree_of_full_dimensional
Proof 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
hs : AffineIndependent ℝ Subtype.val
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
⊢ (convexHull ℝ) ↑s \ combiFrontier ℝ s = interior ((convexHull ℝ) ↑s)
Tactic:
sorry
Proof state after:
no goals
Theorem: frontiers_agree_of_full_dimensional
Proof 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
Proof 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)
Theorem: frontiers_agree_of_full_dimensional
Proof 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
Proof 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
Theorem: frontiers_agree_of_full_dimensional
Proof 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
Proof 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)
Theorem: frontiers_agree_of_full_dimensional
Proof 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]
Proof 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)
Theorem: frontiers_agree_of_full_dimensional
Proof 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⟩
Proof 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)
Theorem: frontiers_agree_of_full_dimensional
Proof 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
Proof 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)
Theorem: frontiers_agree_of_full_dimensional
Proof 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)
Proof state after:
no goals
Theorem: frontiers_agree_of_full_dimensional
Proof 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
Proof 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
Theorem: frontiers_agree_of_full_dimensional
Proof 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
Proof state after:
no goals
Theorem: frontiers_agree_of_full_dimensional
Proof 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⟩
Proof 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
Theorem: frontiers_agree_of_full_dimensional
Proof 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
Proof state after:
no goals
Theorem: subset_closure_combiInterior
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
⊢ ↑s ⊆ closure (combiInterior ℝ s)
Tactic:
rintro x (hx : x ∈ s)
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
⊢ x ∈ closure (combiInterior ℝ s)
Theorem: subset_closure_combiInterior
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
⊢ x ∈ closure (combiInterior ℝ s)
Tactic:
apply seqClosure_subset_closure
Proof state after:
case a
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
⊢ x ∈ seqClosure (combiInterior ℝ s)
Theorem: subset_closure_combiInterior
Proof state before:
case a
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
⊢ x ∈ seqClosure (combiInterior ℝ s)
Tactic:
have hsnonempty : s.Nonempty := ⟨x, hx⟩
Proof state after:
case a
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
⊢ x ∈ seqClosure (combiInterior ℝ s)
Theorem: subset_closure_combiInterior
Proof state before:
case a
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
⊢ x ∈ seqClosure (combiInterior ℝ s)
Tactic:
have centroid_weights : ∑ i : E in s, Finset.centroidWeights ℝ s i = 1 := by
  apply Finset.sum_centroidWeights_eq_one_of_nonempty ℝ _ hsnonempty
Proof state after:
case a
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ x ∈ seqClosure (combiInterior ℝ s)
Theorem: subset_closure_combiInterior
Proof state before:
case a
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ x ∈ seqClosure (combiInterior ℝ s)
Tactic:
refine' ⟨fun n => _, fun n => _, _⟩
Proof state after:
case a.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ E

case a.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (fun n => ?m.106180 n) n ∈ combiInterior ℝ s

case a.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun n => ?m.106180 n) Filter.atTop (nhds x)
Theorem: subset_closure_combiInterior
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
⊢ ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
Tactic:
apply Finset.sum_centroidWeights_eq_one_of_nonempty ℝ _ hsnonempty
Proof state after:
no goals
Theorem: subset_closure_combiInterior
Proof state before:
case a.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ E
Tactic:
apply ((n : ℝ) + 2)⁻¹ • s.centroid ℝ id + (1 - ((n : ℝ) + 2)⁻¹) • x
Proof state after:
no goals
Theorem: subset_closure_combiInterior
Proof state before:
case a.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (fun n => (↑n + 2)⁻¹ • Finset.centroid ℝ s id + (1 - (↑n + 2)⁻¹) • x) n ∈ combiInterior ℝ s
Tactic:
rw [Finset.centroid_def]
Proof state after:
case a.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (fun n => (↑n + 2)⁻¹ • (Finset.affineCombination ℝ s id) (Finset.centroidWeights ℝ s) + (1 - (↑n + 2)⁻¹) • x) n ∈
    combiInterior ℝ s