Theorem: closure_eq_closure_interior (LeanCamCombi/Mathlib/Analysis/Convex/Extreme.lean)

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)
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)

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
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)

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 ⊢
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)

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
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)

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 => _, _⟩
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)

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
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)

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]
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))

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 _)
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

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]
State after:
no goals

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 ⊢
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

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
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

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₁
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

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⟩
State after:
no goals

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
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

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

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