Theorem: frontier_extreme (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
hA₁ : Convex 𝕜 s
hA₂ : IsClosed s
⊢ IsExtreme 𝕜 s (frontier s)
Tactic:
convert
  (inter_frontier_self_inter_convexHull_extreme :
    IsExtreme 𝕜 (closure s) (closure s ∩ frontier (convexHull 𝕜 s))) using 1
State after:
case h.e'_6
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hA₁ : Convex 𝕜 s
hA₂ : IsClosed s
⊢ s = closure s

case h.e'_7
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hA₁ : Convex 𝕜 s
hA₂ : IsClosed s
⊢ frontier s = closure s ∩ frontier ((convexHull 𝕜) s)

State before:
case h.e'_7
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hA₁ : Convex 𝕜 s
hA₂ : IsClosed s
⊢ frontier s = closure s ∩ frontier ((convexHull 𝕜) s)
Tactic:
rw [Convex.convexHull_eq hA₁, inter_eq_self_of_subset_right frontier_subset_closure]
State after:
no goals

State before:
case h.e'_6
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hA₁ : Convex 𝕜 s
hA₂ : IsClosed s
⊢ s = closure s
Tactic:
exact (IsClosed.closure_eq hA₂).symm
State after:
no goals