Theorem: mem_extreme_set_iff_mem_frontier (LeanCamCombi/Mathlib/Analysis/Convex/Exposed.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
⊢ (∃ t, IsExtreme ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t) ↔ x ∈ s ∧ x ∈ frontier s
Tactic:
use fun ⟨t, hst, hts, hxt⟩ => ⟨hst.1 hxt, hst.subset_frontier hts hxt⟩
State after:
case mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
⊢ x ∈ s ∧ x ∈ frontier s → ∃ t, IsExtreme ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t

State before:
case mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
⊢ x ∈ s ∧ x ∈ frontier s → ∃ t, IsExtreme ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
Tactic:
rintro h
State after:
case mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
h : x ∈ s ∧ x ∈ frontier s
⊢ ∃ t, IsExtreme ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t

State before:
case mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
h : x ∈ s ∧ x ∈ frontier s
⊢ ∃ t, IsExtreme ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
Tactic:
obtain ⟨t, hst, hts, hxt⟩ := (mem_exposed_set_iff_mem_frontier hs₁ hs₂).2 h
State after:
case mpr.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t✝ C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
h : x ∈ s ∧ x ∈ frontier s
t : Set E
hst : IsExposed ℝ s t
hts : ¬s ⊆ t
hxt : x ∈ t
⊢ ∃ t, IsExtreme ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t

State before:
case mpr.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t✝ C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hs₁ : Convex ℝ s
hs₂ : (interior s).Nonempty
h : x ∈ s ∧ x ∈ frontier s
t : Set E
hst : IsExposed ℝ s t
hts : ¬s ⊆ t
hxt : x ∈ t
⊢ ∃ t, IsExtreme ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
Tactic:
exact ⟨t, hst.isExtreme, hts, hxt⟩
State after:
no goals