rintro x hxB
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
⊢ t ⊆ frontier s
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ : E
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
x : E
hxB : x ∈ t
⊢ x ∈ frontier s