internlm/Lean-Github huggingface dataset:
Theorem: inter_frontier_self_inter_convexHull_extreme
Proof state before:
case refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ x₁ : E
hx₁A : x₁ ∈ closure s
x₂ : E
hx₂A : x₂ ∈ closure s
x : E
hxs : x ∈ closure s ∩ frontier ((convexHull 𝕜) s)
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ frontier ((convexHull 𝕜) s)

case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ x₁ : E
hx₁A : x₁ ∈ closure s
x₂ : E
hx₂A : x₂ ∈ closure s
x : E
hxs : x ∈ closure s ∩ frontier ((convexHull 𝕜) s)
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₂ ∈ frontier ((convexHull 𝕜) s)
Tactic:
sorry
Proof state after:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ x₁ : E
hx₁A : x₁ ∈ closure s
x₂ : E
hx₂A : x₂ ∈ closure s
x : E
hxs : x ∈ closure s ∩ frontier ((convexHull 𝕜) s)
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₂ ∈ frontier ((convexHull 𝕜) s)
Theorem: inter_frontier_self_inter_convexHull_extreme
Proof state before:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ x₁ : E
hx₁A : x₁ ∈ closure s
x₂ : E
hx₂A : x₂ ∈ closure s
x : E
hxs : x ∈ closure s ∩ frontier ((convexHull 𝕜) s)
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₂ ∈ frontier ((convexHull 𝕜) s)
Tactic:
sorry
Proof state after:
no goals
Theorem: frontier_extreme
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hA₁ : Convex 𝕜 s
hA₂ : IsClosed s
⊢ IsExtreme 𝕜 s (frontier s)
Tactic:
convert
  (inter_frontier_self_inter_convexHull_extreme :
    IsExtreme 𝕜 (closure s) (closure s ∩ frontier (convexHull 𝕜 s))) using 1
Proof state after:
case h.e'_6
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hA₁ : Convex 𝕜 s
hA₂ : IsClosed s
⊢ s = closure s

case h.e'_7
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hA₁ : Convex 𝕜 s
hA₂ : IsClosed s
⊢ frontier s = closure s ∩ frontier ((convexHull 𝕜) s)
Theorem: frontier_extreme
Proof state before:
case h.e'_7
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hA₁ : Convex 𝕜 s
hA₂ : IsClosed s
⊢ frontier s = closure s ∩ frontier ((convexHull 𝕜) s)
Tactic:
rw [Convex.convexHull_eq hA₁, inter_eq_self_of_subset_right frontier_subset_closure]
Proof state after:
no goals
Theorem: frontier_extreme
Proof state before:
case h.e'_6
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hA₁ : Convex 𝕜 s
hA₂ : IsClosed s
⊢ s = closure s
Tactic:
exact (IsClosed.closure_eq hA₂).symm
Proof state after:
no goals
Theorem: Convex.frontier_extreme_to_closure
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hAconv : Convex 𝕜 s
⊢ IsExtreme 𝕜 (closure s) (frontier s)
Tactic:
use frontier_subset_closure
Proof state after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hAconv : Convex 𝕜 s
⊢ ∀ ⦃x₁ : E⦄,
    x₁ ∈ closure s →
      ∀ ⦃x₂ : E⦄,
        x₂ ∈ closure s → ∀ ⦃x : E⦄, x ∈ frontier s → x ∈ openSegment 𝕜 x₁ x₂ → x₁ ∈ frontier s ∧ x₂ ∈ frontier s
Theorem: Convex.frontier_extreme_to_closure
Proof state before:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hAconv : Convex 𝕜 s
⊢ ∀ ⦃x₁ : E⦄,
    x₁ ∈ closure s →
      ∀ ⦃x₂ : E⦄,
        x₂ ∈ closure s → ∀ ⦃x : E⦄, x ∈ frontier s → x ∈ openSegment 𝕜 x₁ x₂ → x₁ ∈ frontier s ∧ x₂ ∈ frontier s
Tactic:
sorry
Proof state after:
no goals
Theorem: IsExtreme.subset_frontier
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
⊢ t ⊆ frontier s
Tactic:
rintro x hxB
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ : E
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
x : E
hxB : x ∈ t
⊢ x ∈ frontier s
Theorem: IsExtreme.subset_frontier
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ : E
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
x : E
hxB : x ∈ t
⊢ x ∈ frontier s
Tactic:
obtain ⟨y, hyA, hyB⟩ := nonempty_of_ssubset ⟨hAB.1, hBA⟩
Proof state after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ : E
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
x : E
hxB : x ∈ t
y : E
hyA : y ∈ s
hyB : y ∉ t
⊢ x ∈ frontier s
Theorem: IsExtreme.subset_frontier
Proof state before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ : E
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
x : E
hxB : x ∈ t
y : E
hyA : y ∈ s
hyB : y ∉ t
⊢ x ∈ frontier s
Tactic:
rw [frontier_eq_closure_inter_closure]
Proof state after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ : E
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
x : E
hxB : x ∈ t
y : E
hyA : y ∈ s
hyB : y ∉ t
⊢ x ∈ closure s ∩ closure sᶜ
Theorem: IsExtreme.subset_frontier
Proof state before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ : E
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
x : E
hxB : x ∈ t
y : E
hyA : y ∈ s
hyB : y ∉ t
⊢ x ∈ closure s ∩ closure sᶜ
Tactic:
use subset_closure (hAB.1 hxB)
Proof state after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ : E
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
x : E
hxB : x ∈ t
y : E
hyA : y ∈ s
hyB : y ∉ t
⊢ x ∈ closure sᶜ
Theorem: IsExtreme.subset_frontier
Proof state before:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ : E
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
x : E
hxB : x ∈ t
y : E
hyA : y ∈ s
hyB : y ∉ t
⊢ x ∈ closure sᶜ
Tactic:
rw [mem_closure_iff_seq_limit]
Proof state after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ : E
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
x : E
hxB : x ∈ t
y : E
hyA : y ∈ s
hyB : y ∉ t
⊢ ∃ x_1, (∀ (n : ℕ), x_1 n ∈ sᶜ) ∧ Filter.Tendsto x_1 Filter.atTop (nhds x)
Theorem: IsExtreme.subset_frontier
Proof state before:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ : E
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
x : E
hxB : x ∈ t
y : E
hyA : y ∈ s
hyB : y ∉ t
⊢ ∃ x_1, (∀ (n : ℕ), x_1 n ∈ sᶜ) ∧ Filter.Tendsto x_1 Filter.atTop (nhds x)
Tactic:
let z : ℕ → E := fun n => (1 + 1 / n.succ : 𝕜) • x - (1 / n.succ : 𝕜) • y
Proof state after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ : E
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
x : E
hxB : x ∈ t
y : E
hyA : y ∈ s
hyB : y ∉ t
z : ℕ → E := fun n => (1 + 1 / ↑n.succ) • x - (1 / ↑n.succ) • y
⊢ ∃ x_1, (∀ (n : ℕ), x_1 n ∈ sᶜ) ∧ Filter.Tendsto x_1 Filter.atTop (nhds x)
Theorem: IsExtreme.subset_frontier
Proof state before:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ : E
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
x : E
hxB : x ∈ t
y : E
hyA : y ∈ s
hyB : y ∉ t
z : ℕ → E := fun n => (1 + 1 / ↑n.succ) • x - (1 / ↑n.succ) • y
⊢ ∃ x_1, (∀ (n : ℕ), x_1 n ∈ sᶜ) ∧ Filter.Tendsto x_1 Filter.atTop (nhds x)
Tactic:
use z
Proof state after:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ : E
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
x : E
hxB : x ∈ t
y : E
hyA : y ∈ s
hyB : y ∉ t
z : ℕ → E := fun n => (1 + 1 / ↑n.succ) • x - (1 / ↑n.succ) • y
⊢ (∀ (n : ℕ), z n ∈ sᶜ) ∧ Filter.Tendsto z Filter.atTop (nhds x)
Theorem: IsExtreme.subset_frontier
Proof state before:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ : E
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
x : E
hxB : x ∈ t
y : E
hyA : y ∈ s
hyB : y ∉ t
z : ℕ → E := fun n => (1 + 1 / ↑n.succ) • x - (1 / ↑n.succ) • y
⊢ (∀ (n : ℕ), z n ∈ sᶜ) ∧ Filter.Tendsto z Filter.atTop (nhds x)
Tactic:
sorry
Proof state after:
no goals
Theorem: closure_eq_closure_interior
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x : E
s : Set E
hAconv : Convex 𝕜 s
hAnemp : (interior s).Nonempty
⊢ closure s = closure (interior s)
Tactic:
refine' Subset.antisymm (fun x hx => _) (closure_mono interior_subset)
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
hAnemp : (interior s).Nonempty
x : E
hx : x ∈ closure s
⊢ x ∈ closure (interior s)
Theorem: closure_eq_closure_interior
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
hAnemp : (interior s).Nonempty
x : E
hx : x ∈ closure s
⊢ x ∈ closure (interior s)
Tactic:
obtain ⟨y, hy⟩ := hAnemp
Proof state after:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x : E
hx : x ∈ closure s
y : E
hy : y ∈ interior s
⊢ x ∈ closure (interior s)
Theorem: closure_eq_closure_interior
Proof state before:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x : E
hx : x ∈ closure s
y : E
hy : y ∈ interior s
⊢ x ∈ closure (interior s)
Tactic:
rw [mem_closure_iff_seq_limit] at hx ⊢
Proof state after:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x : E
hx : ∃ x_1, (∀ (n : ℕ), x_1 n ∈ s) ∧ Filter.Tendsto x_1 Filter.atTop (nhds x)
y : E
hy : y ∈ interior s
⊢ ∃ x_1, (∀ (n : ℕ), x_1 n ∈ interior s) ∧ Filter.Tendsto x_1 Filter.atTop (nhds x)
Theorem: closure_eq_closure_interior
Proof state before:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x : E
hx : ∃ x_1, (∀ (n : ℕ), x_1 n ∈ s) ∧ Filter.Tendsto x_1 Filter.atTop (nhds x)
y : E
hy : y ∈ interior s
⊢ ∃ x_1, (∀ (n : ℕ), x_1 n ∈ interior s) ∧ Filter.Tendsto x_1 Filter.atTop (nhds x)
Tactic:
obtain ⟨z, hzA, hzx⟩ := hx
Proof state after:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ interior s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
⊢ ∃ x_1, (∀ (n : ℕ), x_1 n ∈ interior s) ∧ Filter.Tendsto x_1 Filter.atTop (nhds x)
Theorem: closure_eq_closure_interior
Proof state before:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ interior s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
⊢ ∃ x_1, (∀ (n : ℕ), x_1 n ∈ interior s) ∧ Filter.Tendsto x_1 Filter.atTop (nhds x)
Tactic:
refine' ⟨fun n => (1 - 1 / (n + 2) : 𝕜) • z n + (1 / (n + 2) : 𝕜) • y, fun n => _, _⟩
Proof state after:
case intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ interior s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
n : ℕ
⊢ (fun n => (1 - 1 / (↑n + 2)) • z n + (1 / (↑n + 2)) • y) n ∈ interior s

case intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ interior s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
⊢ Filter.Tendsto (fun n => (1 - 1 / (↑n + 2)) • z n + (1 / (↑n + 2)) • y) Filter.atTop (nhds x)
Theorem: closure_eq_closure_interior
Proof state before:
case intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ interior s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
⊢ Filter.Tendsto (fun n => (1 - 1 / (↑n + 2)) • z n + (1 / (↑n + 2)) • y) Filter.atTop (nhds x)
Tactic:
have h : Filter.Tendsto (fun n : ℕ => 1 / ((n : 𝕜) + 2)) Filter.atTop (nhds (0 : 𝕜)) := by sorry
Proof state after:
case intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ interior s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
h : Filter.Tendsto (fun n => 1 / (↑n + 2)) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun n => (1 - 1 / (↑n + 2)) • z n + (1 / (↑n + 2)) • y) Filter.atTop (nhds x)
Theorem: closure_eq_closure_interior
Proof state before:
case intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ interior s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
h : Filter.Tendsto (fun n => 1 / (↑n + 2)) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun n => (1 - 1 / (↑n + 2)) • z n + (1 / (↑n + 2)) • y) Filter.atTop (nhds x)
Tactic:
rw [← add_zero x, ← one_smul 𝕜 x, ← zero_smul 𝕜 y]
Proof state after:
case intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ interior s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
h : Filter.Tendsto (fun n => 1 / (↑n + 2)) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun n => (1 - 1 / (↑n + 2)) • z n + (1 / (↑n + 2)) • y) Filter.atTop (nhds (1 • x + 0 • y))
Theorem: closure_eq_closure_interior
Proof state before:
case intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ interior s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
h : Filter.Tendsto (fun n => 1 / (↑n + 2)) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun n => (1 - 1 / (↑n + 2)) • z n + (1 / (↑n + 2)) • y) Filter.atTop (nhds (1 • x + 0 • y))
Tactic:
convert ((h.const_sub _).smul hzx).add (h.smul_const _)
Proof state after:
case h.e'_5.h.e'_3.h.e'_5.h.e'_5
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ interior s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
h : Filter.Tendsto (fun n => 1 / (↑n + 2)) Filter.atTop (nhds 0)
⊢ 1 = 1 - 0
Theorem: closure_eq_closure_interior
Proof state before:
case h.e'_5.h.e'_3.h.e'_5.h.e'_5
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ interior s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
h : Filter.Tendsto (fun n => 1 / (↑n + 2)) Filter.atTop (nhds 0)
⊢ 1 = 1 - 0
Tactic:
rw [sub_zero]
Proof state after:
no goals
Theorem: closure_eq_closure_interior
Proof state before:
case intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ interior s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
n : ℕ
⊢ (fun n => (1 - 1 / (↑n + 2)) • z n + (1 / (↑n + 2)) • y) n ∈ interior s
Tactic:
rw [← closure_diff_frontier] at hy ⊢
Proof state after:
case intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ closure s \ frontier s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
n : ℕ
⊢ (fun n => (1 - 1 / (↑n + 2)) • z n + (1 / (↑n + 2)) • y) n ∈ closure s \ frontier s
Theorem: closure_eq_closure_interior
Proof state before:
case intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ closure s \ frontier s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
n : ℕ
⊢ (fun n => (1 - 1 / (↑n + 2)) • z n + (1 / (↑n + 2)) • y) n ∈ closure s \ frontier s
Tactic:
have h₁ : (1 : 𝕜) < ↑n + 2 := by norm_cast; norm_num
Proof state after:
case intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ closure s \ frontier s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
n : ℕ
h₁ : 1 < ↑n + 2
⊢ (fun n => (1 - 1 / (↑n + 2)) • z n + (1 / (↑n + 2)) • y) n ∈ closure s \ frontier s
Theorem: closure_eq_closure_interior
Proof state before:
case intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ closure s \ frontier s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
n : ℕ
h₁ : 1 < ↑n + 2
⊢ (fun n => (1 - 1 / (↑n + 2)) • z n + (1 / (↑n + 2)) • y) n ∈ closure s \ frontier s
Tactic:
have h₀ := zero_lt_one.trans h₁
Proof state after:
case intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ closure s \ frontier s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
n : ℕ
h₁ : 1 < ↑n + 2
h₀ : 0 < ↑n + 2
⊢ (fun n => (1 - 1 / (↑n + 2)) • z n + (1 / (↑n + 2)) • y) n ∈ closure s \ frontier s
Theorem: closure_eq_closure_interior
Proof state before:
case intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ closure s \ frontier s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
n : ℕ
h₁ : 1 < ↑n + 2
h₀ : 0 < ↑n + 2
⊢ (fun n => (1 - 1 / (↑n + 2)) • z n + (1 / (↑n + 2)) • y) n ∈ closure s \ frontier s
Tactic:
exact
  (hAconv.closure.isExtreme_iff_openSegment_subset_diff.1
        hAconv.frontier_extreme_to_closure).2
    (subset_closure (hzA n)) hy
    ⟨1 - 1 / (n + 2), 1 / (n + 2), sub_pos.2 <| (div_lt_one h₀).2 h₁, div_pos zero_lt_one h₀,
      sub_add_cancel _ _, rfl⟩
Proof state after:
no goals
Theorem: closure_eq_closure_interior
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ closure s \ frontier s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
n : ℕ
⊢ 1 < ↑n + 2
Tactic:
norm_cast
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ closure s \ frontier s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
n : ℕ
⊢ 1 < n + 2
Theorem: closure_eq_closure_interior
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ closure s \ frontier s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
n : ℕ
⊢ 1 < n + 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: closure_eq_closure_interior
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ interior s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
⊢ Filter.Tendsto (fun n => 1 / (↑n + 2)) Filter.atTop (nhds 0)
Tactic:
sorry
Proof state after:
no goals
Theorem: ConvexIndependent.subset_of_convexHull_eq_convexHull
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t✝ : Set E
x : E
s t : Finset E
hs : ConvexIndependent 𝕜 Subtype.val
h : (convexHull 𝕜) ↑s = (convexHull 𝕜) ↑t
⊢ s ⊆ t
Tactic:
rintro x hx
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t✝ : Set E
x✝ : E
s t : Finset E
hs : ConvexIndependent 𝕜 Subtype.val
h : (convexHull 𝕜) ↑s = (convexHull 𝕜) ↑t
x : E
hx : x ∈ s
⊢ x ∈ t
Theorem: ConvexIndependent.subset_of_convexHull_eq_convexHull
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t✝ : Set E
x✝ : E
s t : Finset E
hs : ConvexIndependent 𝕜 Subtype.val
h : (convexHull 𝕜) ↑s = (convexHull 𝕜) ↑t
x : E
hx : x ∈ s
⊢ x ∈ t
Tactic:
have hxextreme := (extremePoints_convexHull_eq_iff_convexIndependent.2 hs).symm.subset hx
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t✝ : Set E
x✝ : E
s t : Finset E
hs : ConvexIndependent 𝕜 Subtype.val
h : (convexHull 𝕜) ↑s = (convexHull 𝕜) ↑t
x : E
hx : x ∈ s
hxextreme : x ∈ extremePoints 𝕜 ((convexHull 𝕜) fun x => x ∈ s.val)
⊢ x ∈ t