case h₁
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b✝ : α
s : Set α
a b : α
hab : a ≠ b
⊢ closure (Ioo a b) ⊆ Icc a b

case h₂
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b✝ : α
s : Set α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure (Ioo a b)
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b✝ : α
s : Set α
a b : α
hab : a ≠ b
⊢ closure (Ioo a b) = Icc a b
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 b : α
hab : a ≠ b
⊢ closure (Ioo a b) ⊆ Icc a b
exact closure_minimal Ioo_subset_Icc_self isClosed_Icc
case h₂.inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b✝ : α
s : Set α
a b : α
hab✝ : a ≠ b
hab : a < b
⊢ Icc a b ⊆ closure (Ioo a b)

case h₂.inr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b✝ : α
s : Set α
a b : α
hab✝ : a ≠ b
hab : b < a
⊢ Icc a b ⊆ closure (Ioo a b)
case h₂
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b✝ : α
s : Set α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure (Ioo a b)
cases' hab.lt_or_lt with hab hab
case h₂.inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b✝ : α
s : Set α
a b : α
hab✝ : a ≠ b
hab : a < b
⊢ {a, b} ⊆ closure (Ioo a b)
case h₂.inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b✝ : α
s : Set α
a b : α
hab✝ : a ≠ b
hab : a < b
⊢ Icc a b ⊆ closure (Ioo a b)
rw [← diff_subset_closure_iff, Icc_diff_Ioo_same hab.le]
case h₂.inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b✝ : α
s : Set α
a b : α
hab✝ : a ≠ b
hab : a < b
hab' : Set.Nonempty (Ioo a b)
⊢ {a, b} ⊆ closure (Ioo a b)
case h₂.inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b✝ : α
s : Set α
a b : α
hab✝ : a ≠ b
hab : a < b
⊢ {a, b} ⊆ closure (Ioo a b)
have hab' : (Ioo a b).Nonempty := nonempty_Ioo.2 hab
case h₂.inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b✝ : α
s : Set α
a b : α
hab✝ : a ≠ b
hab : a < b
hab' : Set.Nonempty (Ioo a b)
⊢ a ∈ closure (Ioo a b) ∧ b ∈ closure (Ioo a b)
case h₂.inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b✝ : α
s : Set α
a b : α
hab✝ : a ≠ b
hab : a < b
hab' : Set.Nonempty (Ioo a b)
⊢ {a, b} ⊆ closure (Ioo a b)
simp only [insert_subset, singleton_subset_iff]
no goals
case h₂.inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b✝ : α
s : Set α
a b : α
hab✝ : a ≠ b
hab : a < b
hab' : Set.Nonempty (Ioo a b)
⊢ a ∈ closure (Ioo a b) ∧ b ∈ closure (Ioo a b)
exact ⟨(isGLB_Ioo hab).mem_closure hab', (isLUB_Ioo hab).mem_closure hab'⟩
case h₂.inr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b✝ : α
s : Set α
a b : α
hab✝ : a ≠ b
hab : b < a
⊢ ∅ ⊆ closure (Ioo a b)
case h₂.inr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b✝ : α
s : Set α
a b : α
hab✝ : a ≠ b
hab : b < a
⊢ Icc a b ⊆ closure (Ioo a b)
rw [Icc_eq_empty_of_lt hab]
no goals
case h₂.inr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b✝ : α
s : Set α
a b : α
hab✝ : a ≠ b
hab : b < a
⊢ ∅ ⊆ closure (Ioo a b)
exact empty_subset _