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