no goals
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
a✝ b✝ : α
s : Set α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a b : α
h : a ≤ b
⊢ frontier (Icc a b) = {a, b}
simp [frontier, h, Icc_diff_Ioo_same]