ι : Type ?u.24429
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Set.Ico a b ⊆ Set.Icc a b
ι : Type ?u.24429
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Ico a b ⊆ Icc a b
rw [← coe_subset, coe_Ico, coe_Icc]
no goals
ι : Type ?u.24429
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Set.Ico a b ⊆ Set.Icc a b
exact Set.Ico_subset_Icc_self