Theorem: IsExtreme.subset_frontier (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
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
⊢ t ⊆ frontier s
Tactic:
rintro x hxB
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

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

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

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

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

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

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

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