use frontier_subset_closure
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hAconv : Convex 𝕜 s
⊢ IsExtreme 𝕜 (closure s) (frontier s)
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hAconv : Convex 𝕜 s
⊢ ∀ ⦃x₁ : E⦄,
    x₁ ∈ closure s →
      ∀ ⦃x₂ : E⦄,
        x₂ ∈ closure s → ∀ ⦃x : E⦄, x ∈ frontier s → x ∈ openSegment 𝕜 x₁ x₂ → x₁ ∈ frontier s ∧ x₂ ∈ frontier s