case h₁
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
a : α
h : Set.Nonempty (Ioi a)
⊢ closure (Ioi a) ⊆ Ici a

case h₂
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
a : α
h : Set.Nonempty (Ioi a)
⊢ Ici a ⊆ closure (Ioi a)
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
a : α
h : Set.Nonempty (Ioi a)
⊢ closure (Ioi a) = Ici a
apply Subset.antisymm
no goals
case h₁
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
a : α
h : Set.Nonempty (Ioi a)
⊢ closure (Ioi a) ⊆ Ici a
exact closure_minimal Ioi_subset_Ici_self isClosed_Ici
case h₂
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
a : α
h : Set.Nonempty (Ioi a)
⊢ a ∈ closure (Ioi a)
case h₂
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
a : α
h : Set.Nonempty (Ioi a)
⊢ Ici a ⊆ closure (Ioi a)
rw [← diff_subset_closure_iff, Ici_diff_Ioi_same, singleton_subset_iff]
no goals
case h₂
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
a : α
h : Set.Nonempty (Ioi a)
⊢ a ∈ closure (Ioi a)
exact isGLB_Ioi.mem_closure h