ι : Type ?u.22266
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h : a₁ < a₂
⊢ Set.Ico a₂ b ⊆ Set.Ioo a₁ b
ι : Type ?u.22266
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h : a₁ < a₂
⊢ Ico a₂ b ⊆ Ioo a₁ b
rw [← coe_subset, coe_Ico, coe_Ioo]
no goals
ι : Type ?u.22266
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h : a₁ < a₂
⊢ Set.Ico a₂ b ⊆ Set.Ioo a₁ b
exact Set.Ico_subset_Ioo_left h