case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
a : α
⊢ Ioc a a ⊆ closure (interior (Ioc a a))

case inr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b✝ : α
s : Set α
a b : α
h : a ≠ b
⊢ Ioc a b ⊆ closure (interior (Ioc a b))
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b✝ : α
s : Set α
a b : α
⊢ Ioc a b ⊆ closure (interior (Ioc a b))
rcases eq_or_ne a b with (rfl | h)
no goals
case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
a : α
⊢ Ioc a a ⊆ closure (interior (Ioc a a))
simp
no goals
case inr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b✝ : α
s : Set α
a b : α
h : a ≠ b
⊢ Ioc a b ⊆ closure (interior (Ioc a b))
calc
  Ioc a b ⊆ Icc a b := Ioc_subset_Icc_self
  _ = closure (Ioo a b) := (closure_Ioo h).symm
  _ ⊆ closure (interior (Ioc a b)) :=
    closure_mono (interior_maximal Ioo_subset_Ioc_self isOpen_Ioo)