E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
⊢ s ⊆ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
⊢ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s)) = s
apply (closure_minimal (convexHull_min extremePoints_subset hAconv) hscomp.isClosed).antisymm
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
⊢ False
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
⊢ s ⊆ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
by_contra hs
case intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : ¬x ∈ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
⊢ False
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
⊢ False
obtain ⟨x, hxA, hxt⟩ := not_subset.1 hs
case intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : ¬x ∈ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
l : E →L[ℝ] ℝ
r : ℝ
hlr : ∀ (a : E), a ∈ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s)) → ↑l a < r
hrx : r < ↑l x
⊢ False
case intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : ¬x ∈ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
⊢ False
obtain ⟨l, r, hlr, hrx⟩ :=
  geometric_hahn_banach_closed_point (convex_convexHull _ _).closure isClosed_closure hxt
case intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : ¬x ∈ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
l : E →L[ℝ] ℝ
r : ℝ
hlr : ∀ (a : E), a ∈ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s)) → ↑l a < r
hrx : r < ↑l x
h : IsExposed ℝ s {y | y ∈ s ∧ ∀ (z : E), z ∈ s → ↑l z ≤ ↑l y}
⊢ False
case intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : ¬x ∈ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
l : E →L[ℝ] ℝ
r : ℝ
hlr : ∀ (a : E), a ∈ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s)) → ↑l a < r
hrx : r < ↑l x
⊢ False
have h : IsExposed ℝ s ({ y ∈ s | ∀ z ∈ s, l z ≤ l y }) := fun _ => ⟨l, rfl⟩
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : ¬x ∈ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
l : E →L[ℝ] ℝ
r : ℝ
hlr : ∀ (a : E), a ∈ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s)) → ↑l a < r
hrx : r < ↑l x
h : IsExposed ℝ s {y | y ∈ s ∧ ∀ (z : E), z ∈ s → ↑l z ≤ ↑l y}
z : E
hzA : z ∈ s
hz : ∀ (y : E), y ∈ s → ↑l y ≤ ↑l z
⊢ False
case intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : ¬x ∈ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
l : E →L[ℝ] ℝ
r : ℝ
hlr : ∀ (a : E), a ∈ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s)) → ↑l a < r
hrx : r < ↑l x
h : IsExposed ℝ s {y | y ∈ s ∧ ∀ (z : E), z ∈ s → ↑l z ≤ ↑l y}
⊢ False
obtain ⟨z, hzA, hz⟩ := hscomp.exists_forall_ge ⟨x, hxA⟩ l.continuous.continuousOn
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : ¬x ∈ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
l : E →L[ℝ] ℝ
r : ℝ
hlr : ∀ (a : E), a ∈ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s)) → ↑l a < r
hrx : r < ↑l x
h : IsExposed ℝ s {y | y ∈ s ∧ ∀ (z : E), z ∈ s → ↑l z ≤ ↑l y}
z : E
hzA : z ∈ s
hz : ∀ (y : E), y ∈ s → ↑l y ≤ ↑l z
y : E
hy : y ∈ extremePoints ℝ {y | y ∈ s ∧ ∀ (z : E), z ∈ s → ↑l z ≤ ↑l y}
⊢ False
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : ¬x ∈ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
l : E →L[ℝ] ℝ
r : ℝ
hlr : ∀ (a : E), a ∈ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s)) → ↑l a < r
hrx : r < ↑l x
h : IsExposed ℝ s {y | y ∈ s ∧ ∀ (z : E), z ∈ s → ↑l z ≤ ↑l y}
z : E
hzA : z ∈ s
hz : ∀ (y : E), y ∈ s → ↑l y ≤ ↑l z
⊢ False
obtain ⟨y, hy⟩ := (h.isCompact hscomp).has_extreme_point ⟨z, hzA, hz⟩
no goals
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : ¬x ∈ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s))
l : E →L[ℝ] ℝ
r : ℝ
hlr : ∀ (a : E), a ∈ closure (↑(convexHull ℝ).toOrderHom (extremePoints ℝ s)) → ↑l a < r
hrx : r < ↑l x
h : IsExposed ℝ s {y | y ∈ s ∧ ∀ (z : E), z ∈ s → ↑l z ≤ ↑l y}
z : E
hzA : z ∈ s
hz : ∀ (y : E), y ∈ s → ↑l y ≤ ↑l z
y : E
hy : y ∈ extremePoints ℝ {y | y ∈ s ∧ ∀ (z : E), z ∈ s → ↑l z ≤ ↑l y}
⊢ False
linarith [hlr _ (subset_closure <| subset_convexHull _ _ <|
  h.isExtreme.extremePoints_subset_extremePoints hy), hy.1.2 x hxA]