no goals
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b✝ : α
s : Set α
a b : α
h : a < b
⊢ frontier (Ioo a b) = {a, b}
rw [frontier, closure_Ioo h.ne, interior_Ioo, Icc_diff_Ioo_same h.le]