The predicate List.Sorted (now deprecated).

@[deprecated List.Pairwise (since := "2025-10-11")]

def List.Sorted {α : Type u} (R : α → α → Prop) : List α → Prop

Sorted r l is the same as List.Pairwise r l and has been deprecated. Consider using any of SortedLE, SortedLT, SortedGE, or SortedGT if the relation you're using is a preorder.

Equations

• @List.Sorted = @List.Pairwise

@[deprecated List.instDecidablePairwise (since := "2025-10-11")]

def List.decidableSorted {α : Type u} {r : α → α → Prop} [DecidableRel r] (l : List α) : Decidable (Sorted r l)

Deprecated decidable instance for Sorted.

Equations

• l.decidableSorted = l.instDecidablePairwise

@[deprecated List.Pairwise.nil (since := "2025-10-11")]

theorem List.sorted_nil {α : Type u} {r : α → α → Prop} : Sorted r []

@[deprecated List.Pairwise.of_cons (since := "2025-10-11")]

theorem List.Sorted.of_cons {α : Type u} {r : α → α → Prop} {a : α} {l : List α} (p : Sorted r (a :: l)) : Sorted r l

@[deprecated List.Pairwise.tail (since := "2025-10-11")]

theorem List.Sorted.tail {α : Type u} {r : α → α → Prop} {l : List α} (h : Sorted r l) : Sorted r l.tail

@[deprecated List.rel_of_pairwise_cons (since := "2025-10-11")]

theorem List.rel_of_sorted_cons {α : Type u} {r : α → α → Prop} {a : α} {l : List α} (p : Sorted r (a :: l)) {a' : α} : a' ∈ l → r a a'

@[deprecated List.pairwise_cons (since := "2025-10-11")]

theorem List.sorted_cons {α : Type u} {r : α → α → Prop} {a : α} {l : List α} : Sorted r (a :: l) ↔ (∀ (a' : α), a' ∈ l → r a a') ∧ Sorted r l

@[deprecated List.Pairwise.filter (since := "2025-10-11")]

theorem List.Sorted.filter {α : Type u} {r : α → α → Prop} {l : List α} (p : α → Bool) : Sorted r l → Sorted r (List.filter p l)

@[deprecated List.pairwise_singleton (since := "2025-10-11")]

theorem List.sorted_singleton {α : Type u} (r : α → α → Prop) (a : α) : Sorted r [a]

@[deprecated List.Pairwise.rel_of_mem_take_of_mem_drop (since := "2025-10-11")]

theorem List.Sorted.rel_of_mem_take_of_mem_drop {α : Type u} {r : α → α → Prop} {l : List α} {x y : α} {i : Nat} (h : Sorted r l) (hx : x ∈ take i l) (hy : y ∈ drop i l) : r x y

@[deprecated List.Pairwise.filterMap (since := "2025-10-11")]

theorem List.Sorted.filterMap {α : Type u} {r : α → α → Prop} {l : List α} (f : α → Option α) {s : α → α → Prop} (H : ∀ (a a' : α), r a a' → ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → s b b') : Sorted r l → Sorted s (List.filterMap f l)