α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) b)
⊢ ∅.val = ∅
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) b)
⊢ filter (fun x => b ≤ x) (Ico a b) = ∅
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_right_le]
no goals
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) b)
⊢ ∅.val = ∅
rfl