Theorem: mem_exposed_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, IsExposed ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t) ↔ x ∈ s ∧ x ∈ frontier s
Tactic:
use fun ⟨t, hst, hts, hxt⟩ => ⟨hst.subset 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, IsExposed ℝ 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, IsExposed ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
Tactic:
rintro ⟨hxA, hxfA⟩
State after:
case mpr.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
hxA : x ∈ s
hxfA : x ∈ frontier s
⊢ ∃ t, IsExposed ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t

State before:
case mpr.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
hxA : x ∈ s
hxfA : x ∈ frontier s
⊢ ∃ t, IsExposed ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
Tactic:
obtain ⟨y, hyA⟩ := id hs₂
State after:
case mpr.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
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
⊢ ∃ t, IsExposed ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t

State before:
case mpr.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
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
⊢ ∃ t, IsExposed ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
Tactic:
obtain ⟨l, hl⟩ := geometric_hahn_banach_open_point (Convex.interior hs₁) isOpen_interior hxfA.2
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
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
⊢ ∃ t, IsExposed ℝ 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
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
⊢ ∃ t, IsExposed ℝ s t ∧ ¬s ⊆ t ∧ x ∈ t
Tactic:
refine'
  ⟨{x ∈ s | ∀ y ∈ s, l y ≤ l x}, fun _ => ⟨l, rfl⟩, fun h =>
    not_le.2 (hl y hyA) ((h (interior_subset hyA)).2 x hxA), hxA, fun z hzA => _⟩
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
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
⊢ l z ≤ l x

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
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
⊢ l z ≤ l x
Tactic:
suffices h : l '' closure (interior s) ⊆ closure (Iio (l x)) by
  rw [closure_Iio, ← closure_eq_closure_interior hs₁ hs₂] at h
  exact h ⟨z, subset_closure hzA, rfl⟩
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
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
⊢ ⇑l '' closure (interior s) ⊆ closure (Iio (l x))

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
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
⊢ ⇑l '' closure (interior s) ⊆ closure (Iio (l x))
Tactic:
refine' (image_closure_subset_closure_image l.continuous).trans $ closure_mono _
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
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
⊢ ⇑l '' interior s ⊆ Iio (l x)

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
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
⊢ ⇑l '' interior s ⊆ Iio (l x)
Tactic:
rintro _ ⟨w, hw, rfl⟩
State after:
case mpr.intro.intro.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
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
w : E
hw : w ∈ interior s
⊢ l w ∈ Iio (l x)

State before:
case mpr.intro.intro.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
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
w : E
hw : w ∈ interior s
⊢ l w ∈ Iio (l x)
Tactic:
exact hl w hw
State after:
no goals

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
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
h : ⇑l '' closure (interior s) ⊆ closure (Iio (l x))
⊢ l z ≤ l x
Tactic:
rw [closure_Iio, ← closure_eq_closure_interior hs₁ hs₂] at h
State after:
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
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
h : ⇑l '' closure s ⊆ Iic (l x)
⊢ l z ≤ l x

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
hxA : x ∈ s
hxfA : x ∈ frontier s
y : E
hyA : y ∈ interior s
l : E →L[ℝ] ℝ
hl : ∀ a ∈ interior s, l a < l x
z : E
hzA : z ∈ s
h : ⇑l '' closure s ⊆ Iic (l x)
⊢ l z ≤ l x
Tactic:
exact h ⟨z, subset_closure hzA, rfl⟩
State after:
no goals