Sorting algorithms on lists

In this file we define the sorting algorithm List.insertionSort r and prove that we have (l.insertionSort r l).Pairwise r under suitable conditions on r.

We then define List.SortedLE, List.SortedGE, List.SortedLT and List.SortedGT, predicates which are equivalent to List.Pairwise when the relation derives from a preorder (but which are defined in terms of the monotonicity predicates).

Insertion sort

def List.orderedInsert {α : Type u_1} (r : α → α → Prop) [DecidableRel r] (a : α) : List α → List α

orderedInsert a l inserts a into l at such that orderedInsert a l is sorted if l is.

Equations

• List.orderedInsert r a [] = [a]
• List.orderedInsert r a (b :: l) = if r a b then a :: b :: l else b :: List.orderedInsert r a l

@[simp]

theorem List.orderedInsert_nil {α : Type u_1} (r : α → α → Prop) [DecidableRel r] (a : α) : orderedInsert r a [] = [a]

@[simp]

theorem List.orderedInsert_cons {α : Type u_1} (r : α → α → Prop) [DecidableRel r] (a b : α) (l : List α) : orderedInsert r a (b :: l) = if r a b then a :: b :: l else b :: orderedInsert r a l

theorem List.orderedInsert_cons_of_le {α : Type u_1} (r : α → α → Prop) [DecidableRel r] {a b : α} (l : List α) (h : r a b) : orderedInsert r a (b :: l) = a :: b :: l

theorem List.orderedInsert_of_not_le {α : Type u_1} (r : α → α → Prop) [DecidableRel r] {a b : α} (l : List α) (h : ¬r a b) : orderedInsert r a (b :: l) = b :: orderedInsert r a l

def List.insertionSort {α : Type u_1} (r : α → α → Prop) [DecidableRel r] : List α → List α

insertionSort l returns l sorted using the insertion sort algorithm.

Equations

• List.insertionSort r = List.foldr (List.orderedInsert r) []

@[simp]

theorem List.insertionSort_nil {α : Type u_1} (r : α → α → Prop) [DecidableRel r] : insertionSort r [] = []

@[simp]

theorem List.insertionSort_cons {α : Type u_1} (r : α → α → Prop) [DecidableRel r] (a : α) (l : List α) : insertionSort r (a :: l) = orderedInsert r a (insertionSort r l)

theorem List.orderedInsert_length {α : Type u_1} (r : α → α → Prop) [DecidableRel r] (L : List α) (a : α) : (orderedInsert r a L).length = L.length + 1

theorem List.orderedInsert_eq_take_drop {α : Type u_1} (r : α → α → Prop) [DecidableRel r] (a : α) (l : List α) : orderedInsert r a l = takeWhile (fun (b : α) => decide ¬r a b) l ++ a :: dropWhile (fun (b : α) => decide ¬r a b) l

An alternative definition of orderedInsert using takeWhile and dropWhile.

theorem List.insertionSort_cons_eq_take_drop {α : Type u_1} (r : α → α → Prop) [DecidableRel r] (a : α) (l : List α) : insertionSort r (a :: l) = takeWhile (fun (b : α) => decide ¬r a b) (insertionSort r l) ++ a :: dropWhile (fun (b : α) => decide ¬r a b) (insertionSort r l)

@[simp]

theorem List.mem_orderedInsert {α : Type u_1} (r : α → α → Prop) [DecidableRel r] {a b : α} {l : List α} : a ∈ orderedInsert r b l ↔ a = b ∨ a ∈ l

theorem List.map_orderedInsert {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [DecidableRel r] [DecidableRel s] (f : α → β) (l : List α) (x : α) (hl₁ : ∀ (a : α), a ∈ l → (r a x ↔ s (f a) (f x))) (hl₂ : ∀ (a : α), a ∈ l → (r x a ↔ s (f x) (f a))) : map f (orderedInsert r x l) = orderedInsert s (f x) (map f l)

theorem List.perm_orderedInsert {α : Type u_1} (r : α → α → Prop) [DecidableRel r] (a : α) (l : List α) : (orderedInsert r a l).Perm (a :: l)

theorem List.orderedInsert_count {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [DecidableEq α] (L : List α) (a b : α) : count a (orderedInsert r b L) = count a L + if b = a then 1 else 0

theorem List.perm_insertionSort {α : Type u_1} (r : α → α → Prop) [DecidableRel r] (l : List α) : (insertionSort r l).Perm l

@[simp]

theorem List.mem_insertionSort {α : Type u_1} (r : α → α → Prop) [DecidableRel r] {l : List α} {x : α} : x ∈ insertionSort r l ↔ x ∈ l

@[simp]

theorem List.length_insertionSort {α : Type u_1} (r : α → α → Prop) [DecidableRel r] (l : List α) : (insertionSort r l).length = l.length

theorem List.insertionSort_cons_of_forall_rel {α : Type u_1} (r : α → α → Prop) [DecidableRel r] {a : α} {l : List α} (h : ∀ (b : α), b ∈ l → r a b) : insertionSort r (a :: l) = a :: insertionSort r l

theorem List.map_insertionSort {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [DecidableRel r] [DecidableRel s] (f : α → β) (l : List α) (hl : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → (r a b ↔ s (f a) (f b))) : map f (insertionSort r l) = insertionSort s (map f l)

theorem List.Pairwise.insertionSort_eq {α : Type u_1} {r : α → α → Prop} [DecidableRel r] {l : List α} : Pairwise r l → insertionSort r l = l

If l is already List.Pairwise with respect to r, then insertionSort does not change it.

theorem List.erase_orderedInsert {α : Type u_1} {r : α → α → Prop} [DecidableRel r] [DecidableEq α] [Std.Refl r] (x : α) (xs : List α) : (orderedInsert r x xs).erase x = xs

For a reflexive relation, insert then erasing is the identity.

theorem List.erase_orderedInsert_of_notMem {α : Type u_1} {r : α → α → Prop} [DecidableRel r] [DecidableEq α] {x : α} {xs : List α} (hx : ¬x ∈ xs) : (orderedInsert r x xs).erase x = xs

Inserting then erasing an element that is absent is the identity.

theorem List.orderedInsert_erase {α : Type u_1} {r : α → α → Prop} [DecidableRel r] [DecidableEq α] [Std.Antisymm r] (x : α) (xs : List α) (hx : x ∈ xs) (hxs : Pairwise r xs) : orderedInsert r x (xs.erase x) = xs

For an antisymmetric relation, erasing then inserting is the identity.

theorem List.sublist_orderedInsert {α : Type u_1} {r : α → α → Prop} [DecidableRel r] (x : α) (xs : List α) : xs.Sublist (orderedInsert r x xs)

theorem List.cons_sublist_orderedInsert {α : Type u_1} {r : α → α → Prop} [DecidableRel r] {l c : List α} {a : α} (hl : c.Sublist l) (ha : ∀ (a' : α), a' ∈ c → r a a') : (a :: c).Sublist (orderedInsert r a l)

theorem List.Sublist.orderedInsert_sublist {α : Type u_1} {r : α → α → Prop} [DecidableRel r] [IsTrans α r] {as bs : List α} (x : α) (hs : as.Sublist bs) (hb : Pairwise r bs) : (orderedInsert r x as).Sublist (orderedInsert r x bs)

theorem List.Pairwise.orderedInsert {α : Type u_1} {r : α → α → Prop} [DecidableRel r] [Std.Total r] [IsTrans α r] (a : α) (l : List α) : Pairwise r l → Pairwise r (List.orderedInsert r a l)

theorem List.pairwise_insertionSort {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [Std.Total r] [IsTrans α r] (l : List α) : Pairwise r (insertionSort r l)

The list List.insertionSort r l is List.Pairwise with respect to r.

theorem List.sublist_insertionSort {α : Type u_1} {r : α → α → Prop} [DecidableRel r] {l c : List α} (hr : Pairwise r c) (hc : c.Sublist l) : c.Sublist (insertionSort r l)

If c is a sorted sublist of l, then c is still a sublist of insertionSort r l.

theorem List.pair_sublist_insertionSort {α : Type u_1} {r : α → α → Prop} [DecidableRel r] {a b : α} {l : List α} (hab : r a b) (h : [a, b].Sublist l) : [a, b].Sublist (insertionSort r l)

Another statement of stability of insertion sort. If a pair [a, b] is a sublist of l and r a b, then [a, b] is still a sublist of insertionSort r l.

theorem List.sublist_insertionSort' {α : Type u_1} {r : α → α → Prop} [DecidableRel r] [Std.Antisymm r] [Std.Total r] [IsTrans α r] {l c : List α} (hs : Pairwise r c) (hc : c.Subperm l) : c.Sublist (insertionSort r l)

A version of insertionSort_stable which only assumes c <+~ l (instead of c <+ l), but additionally requires Std.Antisymm r, Std.Total r and IsTrans α r.

theorem List.pair_sublist_insertionSort' {α : Type u_1} {r : α → α → Prop} [DecidableRel r] [Std.Antisymm r] [Std.Total r] [IsTrans α r] {a b : α} {l : List α} (hab : r a b) (h : [a, b].Subperm l) : [a, b].Sublist (insertionSort r l)

Another statement of stability of insertion sort. If a pair [a, b] is a sublist of a permutation of l and a ≼ b, then [a, b] is still a sublist of insertionSort r l.

Merge sort

We provide some wrapper functions around the theorems for mergeSort provided in Lean, which rather than using explicit hypotheses for transitivity and totality, use Mathlib order typeclasses instead.

theorem List.Perm.eq_of_pairwise' {α : Type u_1} {r : α → α → Prop} [Std.Antisymm r] {l₁ l₂ : List α} : Pairwise r l₁ → Pairwise r l₂ → ∀ (hl : l₁.Perm l₂), l₁ = l₂

Variant of Perm.eq_of_pairwise using relation typeclasses.

theorem List.sublist_of_subperm_of_pairwise {α : Type u_1} {r : α → α → Prop} [Std.Antisymm r] {l₁ l₂ : List α} (hp : l₁.Subperm l₂) (hs₁ : Pairwise r l₁) (hs₂ : Pairwise r l₂) : l₁.Sublist l₂

theorem List.Subset.antisymm_of_pairwise {α : Type u_1} {r : α → α → Prop} [Std.Antisymm r] [Std.Irrefl r] {l₁ l₂ : List α} (h₁ : Pairwise r l₁) (h₂ : Pairwise r l₂) (hl₁₂ : l₁ ⊆ l₂) (hl₁₂' : l₂ ⊆ l₁) : l₁ = l₂

theorem List.Pairwise.eq_of_mem_iff {α : Type u_1} {r : α → α → Prop} [Std.Antisymm r] [Std.Irrefl r] {l₁ l₂ : List α} (h₁ : Pairwise r l₁) (h₂ : Pairwise r l₂) (h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂) : l₁ = l₂

theorem List.Pairwise.merge {α : Type u_1} {r : α → α → Prop} [DecidableRel r] [Std.Total r] [IsTrans α r] {l l' : List α} (h : Pairwise r l) (h' : Pairwise r l') : Pairwise r (l.merge l' fun (x1 x2 : α) => decide (r x1 x2))

theorem List.pairwise_mergeSort' {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [Std.Total r] [IsTrans α r] (l : List α) : Pairwise r (l.mergeSort fun (x1 x2 : α) => decide (r x1 x2))

Variant of pairwise_mergeSort using relation typeclasses.

theorem List.mergeSort_eq_self {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [Std.Total r] [IsTrans α r] [Std.Antisymm r] {l : List α} : Pairwise r l → (l.mergeSort fun (x1 x2 : α) => decide (r x1 x2)) = l

theorem List.mergeSort_eq_insertionSort {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [Std.Total r] [IsTrans α r] [Std.Antisymm r] (l : List α) : (l.mergeSort fun (x1 x2 : α) => decide (r x1 x2)) = insertionSort r l

The predicates List.SortedLE, List.SortedGE, List.SortedLT and List.SortedGT

These predicates are equivalent to Monotone l.get, but they are also equivalent to IsChain (· < ·) and Pairwise (· < ·). API is provided to move between these forms.

API has deliberately not been provided for decomposed lists to avoid unneeded API replication. The provided API should be used to move to and from IsChain, Pairwise or Monotone as needed.

def List.SortedLE {α : Type u_1} [Preorder α] (l : List α) : Prop

l.SortedLE means that the list is monotonic.

Equations

• l.SortedLE = Monotone l.get

def List.SortedGE {α : Type u_1} [Preorder α] (l : List α) : Prop

l.SortedGE means that the list is antitonic.

Equations

• l.SortedGE = Antitone l.get

def List.SortedLT {α : Type u_1} [Preorder α] (l : List α) : Prop

l.SortedLT means that the list is strictly monotonic.

Equations

• l.SortedLT = StrictMono l.get

def List.SortedGT {α : Type u_1} [Preorder α] (l : List α) : Prop

l.SortedGT means that the list is strictly antitonic.

Equations

• l.SortedGT = StrictAnti l.get

theorem List.sortedLE_iff_monotone_get {α : Type u_1} {l : List α} [Preorder α] : l.SortedLE ↔ Monotone l.get

theorem List.sortedGE_iff_antitone_get {α : Type u_1} {l : List α} [Preorder α] : l.SortedGE ↔ Antitone l.get

theorem List.sortedLT_iff_strictMono_get {α : Type u_1} {l : List α} [Preorder α] : l.SortedLT ↔ StrictMono l.get

theorem List.sortedGT_iff_strictAnti_get {α : Type u_1} {l : List α} [Preorder α] : l.SortedGT ↔ StrictAnti l.get

theorem List.SortedLE.monotone_get {α : Type u_1} {l : List α} [Preorder α] : l.SortedLE → Monotone l.get

Alias of the forward direction of List.sortedLE_iff_monotone_get.

theorem Monotone.sortedLE {α : Type u_1} {l : List α} [Preorder α] : Monotone l.get → l.SortedLE

Alias of the reverse direction of List.sortedLE_iff_monotone_get.

theorem Antitone.sortedGE {α : Type u_1} {l : List α} [Preorder α] : Antitone l.get → l.SortedGE

Alias of the reverse direction of List.sortedGE_iff_antitone_get.

theorem List.SortedGE.antitone_get {α : Type u_1} {l : List α} [Preorder α] : l.SortedGE → Antitone l.get

Alias of the forward direction of List.sortedGE_iff_antitone_get.

theorem List.SortedLT.strictMono_get {α : Type u_1} {l : List α} [Preorder α] : l.SortedLT → StrictMono l.get

Alias of the forward direction of List.sortedLT_iff_strictMono_get.

theorem StrictMono.sortedLT {α : Type u_1} {l : List α} [Preorder α] : StrictMono l.get → l.SortedLT

Alias of the reverse direction of List.sortedLT_iff_strictMono_get.

theorem StrictAnti.sortedGT {α : Type u_1} {l : List α} [Preorder α] : StrictAnti l.get → l.SortedGT

Alias of the reverse direction of List.sortedGT_iff_strictAnti_get.

theorem List.SortedGT.strictAnti_get {α : Type u_1} {l : List α} [Preorder α] : l.SortedGT → StrictAnti l.get

Alias of the forward direction of List.sortedGT_iff_strictAnti_get.

theorem List.sortedLE_iff_pairwise {α : Type u_1} {l : List α} [Preorder α] : l.SortedLE ↔ Pairwise (fun (x1 x2 : α) => x1 ≤ x2) l

theorem List.sortedGE_iff_pairwise {α : Type u_1} {l : List α} [Preorder α] : l.SortedGE ↔ Pairwise (fun (x1 x2 : α) => x1 ≥ x2) l

theorem List.sortedLT_iff_pairwise {α : Type u_1} {l : List α} [Preorder α] : l.SortedLT ↔ Pairwise (fun (x1 x2 : α) => x1 < x2) l

theorem List.sortedGT_iff_pairwise {α : Type u_1} {l : List α} [Preorder α] : l.SortedGT ↔ Pairwise (fun (x1 x2 : α) => x1 > x2) l

theorem List.SortedLE.pairwise {α : Type u_1} {l : List α} [Preorder α] : l.SortedLE → Pairwise (fun (x1 x2 : α) => x1 ≤ x2) l

Alias of the forward direction of List.sortedLE_iff_pairwise.

theorem List.Pairwise.sortedLE {α : Type u_1} {l : List α} [Preorder α] : Pairwise (fun (x1 x2 : α) => x1 ≤ x2) l → l.SortedLE

Alias of the reverse direction of List.sortedLE_iff_pairwise.

theorem List.SortedGE.pairwise {α : Type u_1} {l : List α} [Preorder α] : l.SortedGE → Pairwise (fun (x1 x2 : α) => x1 ≥ x2) l

Alias of the forward direction of List.sortedGE_iff_pairwise.

theorem List.Pairwise.sortedGE {α : Type u_1} {l : List α} [Preorder α] : Pairwise (fun (x1 x2 : α) => x1 ≥ x2) l → l.SortedGE

Alias of the reverse direction of List.sortedGE_iff_pairwise.

theorem List.SortedLT.pairwise {α : Type u_1} {l : List α} [Preorder α] : l.SortedLT → Pairwise (fun (x1 x2 : α) => x1 < x2) l

Alias of the forward direction of List.sortedLT_iff_pairwise.

theorem List.Pairwise.sortedLT {α : Type u_1} {l : List α} [Preorder α] : Pairwise (fun (x1 x2 : α) => x1 < x2) l → l.SortedLT

Alias of the reverse direction of List.sortedLT_iff_pairwise.

theorem List.SortedGT.pairwise {α : Type u_1} {l : List α} [Preorder α] : l.SortedGT → Pairwise (fun (x1 x2 : α) => x1 > x2) l

Alias of the forward direction of List.sortedGT_iff_pairwise.

theorem List.Pairwise.sortedGT {α : Type u_1} {l : List α} [Preorder α] : Pairwise (fun (x1 x2 : α) => x1 > x2) l → l.SortedGT

Alias of the reverse direction of List.sortedGT_iff_pairwise.

theorem List.sortedLE_iff_isChain {α : Type u_1} {l : List α} [Preorder α] : l.SortedLE ↔ IsChain (fun (x1 x2 : α) => x1 ≤ x2) l

theorem List.sortedGE_iff_isChain {α : Type u_1} {l : List α} [Preorder α] : l.SortedGE ↔ IsChain (fun (x1 x2 : α) => x1 ≥ x2) l

theorem List.sortedLT_iff_isChain {α : Type u_1} {l : List α} [Preorder α] : l.SortedLT ↔ IsChain (fun (x1 x2 : α) => x1 < x2) l

theorem List.sortedGT_iff_isChain {α : Type u_1} {l : List α} [Preorder α] : l.SortedGT ↔ IsChain (fun (x1 x2 : α) => x1 > x2) l

theorem List.IsChain.sortedLE {α : Type u_1} {l : List α} [Preorder α] : IsChain (fun (x1 x2 : α) => x1 ≤ x2) l → l.SortedLE

Alias of the reverse direction of List.sortedLE_iff_isChain.

theorem List.SortedLE.isChain {α : Type u_1} {l : List α} [Preorder α] : l.SortedLE → IsChain (fun (x1 x2 : α) => x1 ≤ x2) l

Alias of the forward direction of List.sortedLE_iff_isChain.

theorem List.SortedGE.isChain {α : Type u_1} {l : List α} [Preorder α] : l.SortedGE → IsChain (fun (x1 x2 : α) => x1 ≥ x2) l

Alias of the forward direction of List.sortedGE_iff_isChain.

theorem List.IsChain.sortedGE {α : Type u_1} {l : List α} [Preorder α] : IsChain (fun (x1 x2 : α) => x1 ≥ x2) l → l.SortedGE

Alias of the reverse direction of List.sortedGE_iff_isChain.

theorem List.SortedLT.isChain {α : Type u_1} {l : List α} [Preorder α] : l.SortedLT → IsChain (fun (x1 x2 : α) => x1 < x2) l

Alias of the forward direction of List.sortedLT_iff_isChain.

theorem List.IsChain.sortedLT {α : Type u_1} {l : List α} [Preorder α] : IsChain (fun (x1 x2 : α) => x1 < x2) l → l.SortedLT

Alias of the reverse direction of List.sortedLT_iff_isChain.

theorem List.IsChain.sortedGT {α : Type u_1} {l : List α} [Preorder α] : IsChain (fun (x1 x2 : α) => x1 > x2) l → l.SortedGT

Alias of the reverse direction of List.sortedGT_iff_isChain.

theorem List.SortedGT.isChain {α : Type u_1} {l : List α} [Preorder α] : l.SortedGT → IsChain (fun (x1 x2 : α) => x1 > x2) l

Alias of the forward direction of List.sortedGT_iff_isChain.

@[instance_reducible]

instance List.decidableSortedLE {α : Type u_1} [Preorder α] [DecidableLE α] : DecidablePred SortedLE

Equations

• x✝.decidableSortedLE = decidable_of_iff' (List.IsChain (fun (x1 x2 : α) => x1 ≤ x2) x✝) ⋯

@[instance_reducible]

instance List.decidableSortedGE {α : Type u_1} [Preorder α] [DecidableLE α] : DecidablePred SortedGE

Equations

• x✝.decidableSortedGE = decidable_of_iff' (List.IsChain (fun (x1 x2 : α) => x1 ≥ x2) x✝) ⋯

@[instance_reducible]

instance List.decidableSortedLT {α : Type u_1} [Preorder α] [DecidableLT α] : DecidablePred SortedLT

Equations

• x✝.decidableSortedLT = decidable_of_iff' (List.IsChain (fun (x1 x2 : α) => x1 < x2) x✝) ⋯

@[instance_reducible]

instance List.decidableSortedGT {α : Type u_1} [Preorder α] [DecidableLT α] : DecidablePred SortedGT

Equations

• x✝.decidableSortedGT = decidable_of_iff' (List.IsChain (fun (x1 x2 : α) => x1 > x2) x✝) ⋯

theorem List.sortedLE_iff_getElem_le_getElem_of_le {α : Type u_1} {l : List α} [Preorder α] : l.SortedLE ↔ ∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, i ≤ j → l[i] ≤ l[j]

theorem List.sortedGE_iff_getElem_ge_getElem_of_le {α : Type u_1} {l : List α} [Preorder α] : l.SortedGE ↔ ∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, j ≤ i → l[i] ≤ l[j]

theorem List.sortedLT_iff_getElem_lt_getElem_of_lt {α : Type u_1} {l : List α} [Preorder α] : l.SortedLT ↔ ∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, i < j → l[i] < l[j]

theorem List.sortedGT_iff_getElem_gt_getElem_of_lt {α : Type u_1} {l : List α} [Preorder α] : l.SortedGT ↔ ∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, j < i → l[i] < l[j]

theorem List.SortedLE.getElem_le_getElem_of_le {α : Type u_1} {l : List α} [Preorder α] : l.SortedLE → ∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, i ≤ j → l[i] ≤ l[j]

Alias of the forward direction of List.sortedLE_iff_getElem_le_getElem_of_le.

theorem List.sortedLE_of_getElem_le_getElem_of_le {α : Type u_1} {l : List α} [Preorder α] : (∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, i ≤ j → l[i] ≤ l[j]) → l.SortedLE

Alias of the reverse direction of List.sortedLE_iff_getElem_le_getElem_of_le.

theorem List.sortedGE_of_getElem_ge_getElem_of_le {α : Type u_1} {l : List α} [Preorder α] : (∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, j ≤ i → l[i] ≤ l[j]) → l.SortedGE

Alias of the reverse direction of List.sortedGE_iff_getElem_ge_getElem_of_le.

theorem List.SortedGE.getElem_ge_getElem_of_le {α : Type u_1} {l : List α} [Preorder α] : l.SortedGE → ∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, j ≤ i → l[i] ≤ l[j]

Alias of the forward direction of List.sortedGE_iff_getElem_ge_getElem_of_le.

theorem List.sortedLT_of_getElem_lt_getElem_of_lt {α : Type u_1} {l : List α} [Preorder α] : (∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, i < j → l[i] < l[j]) → l.SortedLT

Alias of the reverse direction of List.sortedLT_iff_getElem_lt_getElem_of_lt.

theorem List.SortedLT.getElem_lt_getElem_of_lt {α : Type u_1} {l : List α} [Preorder α] : l.SortedLT → ∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, i < j → l[i] < l[j]

Alias of the forward direction of List.sortedLT_iff_getElem_lt_getElem_of_lt.

theorem List.sortedGT_of_getElem_gt_getElem_of_lt {α : Type u_1} {l : List α} [Preorder α] : (∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, j < i → l[i] < l[j]) → l.SortedGT

Alias of the reverse direction of List.sortedGT_iff_getElem_gt_getElem_of_lt.

theorem List.SortedGT.getElem_gt_getElem_of_lt {α : Type u_1} {l : List α} [Preorder α] : l.SortedGT → ∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, j < i → l[i] < l[j]

Alias of the forward direction of List.sortedGT_iff_getElem_gt_getElem_of_lt.

theorem List.SortedLT.sortedLE {α : Type u_1} [Preorder α] {l : List α} (h : l.SortedLT) : l.SortedLE

theorem List.SortedGT.sortedGE {α : Type u_1} [Preorder α] {l : List α} (h : l.SortedGT) : l.SortedGE

theorem List.SortedLT.nodup {α : Type u_1} {l : List α} [Preorder α] (h : l.SortedLT) : l.Nodup

theorem List.SortedGT.nodup {α : Type u_1} {l : List α} [Preorder α] (h : l.SortedGT) : l.Nodup

theorem List.sortedLE_replicate {α : Type u_1} [Preorder α] {a : α} (n : ℕ) : (replicate n a).SortedLE

theorem List.sortedLT_finRange (n : ℕ) : (finRange n).SortedLT

theorem List.sortedLT_range (n : ℕ) : (range n).SortedLT

theorem List.sortedLT_range' (a b : ℕ) {s : ℕ} (hs : s ≠ 0) : (range' a b s).SortedLT

theorem List.sortedLE_range' (a b s : ℕ) : (range' a b s).SortedLE

@[simp]

theorem List.sortedLE_ofFn_iff {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin n → α} : (ofFn f).SortedLE ↔ Monotone f

The list List.ofFn f is sorted with respect to (· ≤ ·) if and only if f is monotone.

@[simp]

theorem List.sortedGE_ofFn_iff {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin n → α} : (ofFn f).SortedGE ↔ Antitone f

The list List.ofFn f is sorted with respect to (· ≥ ·) if and only if f is antitone.

@[simp]

theorem List.sortedLT_ofFn_iff {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin n → α} : (ofFn f).SortedLT ↔ StrictMono f

The list List.ofFn f is strictly sorted with respect to (· ≤ ·) if and only if f is strictly monotone.

@[simp]

theorem List.sortedGT_ofFn_iff {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin n → α} : (ofFn f).SortedGT ↔ StrictAnti f

The list List.ofFn f is strictly sorted with respect to (· ≥ ·) if and only if f is strictly antitone.

theorem Monotone.sortedLE_ofFn {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin n → α} : Monotone f → (List.ofFn f).SortedLE

The list obtained from a monotone tuple is sorted.

theorem List.SortedLE.monotone {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin n → α} : (ofFn f).SortedLE → Monotone f

The list obtained from a monotone tuple is sorted.

theorem List.SortedGE.antitone {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin n → α} : (ofFn f).SortedGE → Antitone f

The list obtained from an antitone tuple is sorted.

theorem Antitone.sortedGE_ofFn {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin n → α} : Antitone f → (List.ofFn f).SortedGE

The list obtained from an antitone tuple is sorted.

theorem StrictMono.sortedLT_ofFn {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin n → α} : StrictMono f → (List.ofFn f).SortedLT

The list obtained from a strictly monotone tuple is sorted.

theorem List.SortedLT.strictMono {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin n → α} : (ofFn f).SortedLT → StrictMono f

The list obtained from a strictly monotone tuple is sorted.

theorem StrictAnti.sortedGT_ofFn {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin n → α} : StrictAnti f → (List.ofFn f).SortedGT

The list obtained from a strictly antitone tuple is sorted.

theorem List.SortedGT.strictAnti {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin n → α} : (ofFn f).SortedGT → StrictAnti f

The list obtained from a strictly antitone tuple is sorted.

@[simp]

theorem List.sortedLE_reverse {α : Type u_1} {l : List α} [Preorder α] : l.reverse.SortedLE ↔ l.SortedGE

@[simp]

theorem List.sortedGE_reverse {α : Type u_1} {l : List α} [Preorder α] : l.reverse.SortedGE ↔ l.SortedLE

@[simp]

theorem List.sortedLT_reverse {α : Type u_1} {l : List α} [Preorder α] : l.reverse.SortedLT ↔ l.SortedGT

@[simp]

theorem List.sortedGT_reverse {α : Type u_1} {l : List α} [Preorder α] : l.reverse.SortedGT ↔ l.SortedLT

theorem List.SortedGE.reverse {α : Type u_1} {l : List α} [Preorder α] : l.SortedGE → l.reverse.SortedLE

Alias of the reverse direction of List.sortedLE_reverse.

theorem List.SortedLE.of_reverse {α : Type u_1} {l : List α} [Preorder α] : l.reverse.SortedLE → l.SortedGE

Alias of the forward direction of List.sortedLE_reverse.

theorem List.SortedLE.reverse {α : Type u_1} {l : List α} [Preorder α] : l.SortedLE → l.reverse.SortedGE

Alias of the reverse direction of List.sortedGE_reverse.

theorem List.SortedGE.of_reverse {α : Type u_1} {l : List α} [Preorder α] : l.reverse.SortedGE → l.SortedLE

Alias of the forward direction of List.sortedGE_reverse.

theorem List.SortedLT.of_reverse {α : Type u_1} {l : List α} [Preorder α] : l.reverse.SortedLT → l.SortedGT

Alias of the forward direction of List.sortedLT_reverse.

theorem List.SortedGT.reverse {α : Type u_1} {l : List α} [Preorder α] : l.SortedGT → l.reverse.SortedLT

Alias of the reverse direction of List.sortedLT_reverse.

theorem List.SortedGT.of_reverse {α : Type u_1} {l : List α} [Preorder α] : l.reverse.SortedGT → l.SortedLT

Alias of the forward direction of List.sortedGT_reverse.

theorem List.SortedLT.reverse {α : Type u_1} {l : List α} [Preorder α] : l.SortedLT → l.reverse.SortedGT

Alias of the reverse direction of List.sortedGT_reverse.

@[simp]

theorem List.sortedLE_map_ofDual {α : Type u_1} [Preorder α] {l : List αᵒᵈ} : (map (⇑OrderDual.ofDual) l).SortedLE ↔ l.SortedGE

@[simp]

theorem List.sortedGE_map_ofDual {α : Type u_1} [Preorder α] {l : List αᵒᵈ} : (map (⇑OrderDual.ofDual) l).SortedGE ↔ l.SortedLE

@[simp]

theorem List.sortedLT_map_ofDual {α : Type u_1} [Preorder α] {l : List αᵒᵈ} : (map (⇑OrderDual.ofDual) l).SortedLT ↔ l.SortedGT

@[simp]

theorem List.sortedGT_map_ofDual {α : Type u_1} [Preorder α] {l : List αᵒᵈ} : (map (⇑OrderDual.ofDual) l).SortedGT ↔ l.SortedLT

theorem List.SortedLE.map_ofDual {α : Type u_1} [Preorder α] {l : List αᵒᵈ} : (map (⇑OrderDual.ofDual) l).SortedLE → l.SortedGE

Alias of the forward direction of List.sortedLE_map_ofDual.

theorem List.SortedGE.of_map_ofDual {α : Type u_1} [Preorder α] {l : List αᵒᵈ} : l.SortedGE → (map (⇑OrderDual.ofDual) l).SortedLE

Alias of the reverse direction of List.sortedLE_map_ofDual.

theorem List.SortedLE.of_map_ofDual {α : Type u_1} [Preorder α] {l : List αᵒᵈ} : l.SortedLE → (map (⇑OrderDual.ofDual) l).SortedGE

Alias of the reverse direction of List.sortedGE_map_ofDual.

theorem List.SortedGE.map_ofDual {α : Type u_1} [Preorder α] {l : List αᵒᵈ} : (map (⇑OrderDual.ofDual) l).SortedGE → l.SortedLE

Alias of the forward direction of List.sortedGE_map_ofDual.

theorem List.SortedLT.map_ofDual {α : Type u_1} [Preorder α] {l : List αᵒᵈ} : (map (⇑OrderDual.ofDual) l).SortedLT → l.SortedGT

Alias of the forward direction of List.sortedLT_map_ofDual.

theorem List.SortedGT.of_map_ofDual {α : Type u_1} [Preorder α] {l : List αᵒᵈ} : l.SortedGT → (map (⇑OrderDual.ofDual) l).SortedLT

Alias of the reverse direction of List.sortedLT_map_ofDual.

theorem List.SortedGT.map_ofDual {α : Type u_1} [Preorder α] {l : List αᵒᵈ} : (map (⇑OrderDual.ofDual) l).SortedGT → l.SortedLT

Alias of the forward direction of List.sortedGT_map_ofDual.

theorem List.SortedLT.of_map_ofDual {α : Type u_1} [Preorder α] {l : List αᵒᵈ} : l.SortedLT → (map (⇑OrderDual.ofDual) l).SortedGT

Alias of the reverse direction of List.sortedGT_map_ofDual.

theorem List.sortedLE_map_toDual {α : Type u_1} [Preorder α] {l : List α} : (map (⇑OrderDual.toDual) l).SortedLE ↔ l.SortedGE

theorem List.sortedGE_map_toDual {α : Type u_1} [Preorder α] {l : List α} : (map (⇑OrderDual.toDual) l).SortedGE ↔ l.SortedLE

theorem List.sortedLT_map_toDual {α : Type u_1} [Preorder α] {l : List α} : (map (⇑OrderDual.toDual) l).SortedLT ↔ l.SortedGT

theorem List.sortedGT_map_toDual {α : Type u_1} [Preorder α] {l : List αᵒᵈ} : (map (⇑OrderDual.toDual) l).SortedGT ↔ l.SortedLT

theorem List.SortedGE.of_map_toDual {α : Type u_1} [Preorder α] {l : List α} : l.SortedGE → (map (⇑OrderDual.toDual) l).SortedLE

Alias of the reverse direction of List.sortedLE_map_toDual.

theorem List.SortedLE.map_toDual {α : Type u_1} [Preorder α] {l : List α} : (map (⇑OrderDual.toDual) l).SortedLE → l.SortedGE

Alias of the forward direction of List.sortedLE_map_toDual.

theorem List.SortedGE.map_toDual {α : Type u_1} [Preorder α] {l : List α} : (map (⇑OrderDual.toDual) l).SortedGE → l.SortedLE

Alias of the forward direction of List.sortedGE_map_toDual.

theorem List.SortedLE.of_map_toDual {α : Type u_1} [Preorder α] {l : List α} : l.SortedLE → (map (⇑OrderDual.toDual) l).SortedGE

Alias of the reverse direction of List.sortedGE_map_toDual.

theorem List.SortedLT.map_toDual {α : Type u_1} [Preorder α] {l : List α} : (map (⇑OrderDual.toDual) l).SortedLT → l.SortedGT

Alias of the forward direction of List.sortedLT_map_toDual.

theorem List.SortedGT.of_map_toDual {α : Type u_1} [Preorder α] {l : List α} : l.SortedGT → (map (⇑OrderDual.toDual) l).SortedLT

Alias of the reverse direction of List.sortedLT_map_toDual.

theorem List.SortedLT.of_map_toDual {α : Type u_1} [Preorder α] {l : List αᵒᵈ} : l.SortedLT → (map (⇑OrderDual.toDual) l).SortedGT

Alias of the reverse direction of List.sortedGT_map_toDual.

theorem List.SortedGT.map_toDual {α : Type u_1} [Preorder α] {l : List αᵒᵈ} : (map (⇑OrderDual.toDual) l).SortedGT → l.SortedLT

Alias of the forward direction of List.sortedGT_map_toDual.

theorem List.SortedLE.sortedLT_of_nodup {α : Type u_1} [PartialOrder α] {l : List α} (h₁ : l.SortedLE) (h₂ : l.Nodup) : l.SortedLT

theorem List.SortedGE.sortedGT_of_nodup {α : Type u_1} [PartialOrder α] {l : List α} (h₁ : l.SortedGE) (h₂ : l.Nodup) : l.SortedGT

theorem List.sortedLT_iff_nodup_and_sortedLE {α : Type u_1} {l : List α} [PartialOrder α] : l.SortedLT ↔ l.Nodup ∧ l.SortedLE

theorem List.sortedGT_iff_nodup_and_sortedGE {α : Type u_1} {l : List α} [PartialOrder α] : l.SortedGT ↔ l.Nodup ∧ l.SortedGE

theorem List.Perm.eq_of_sortedLE {α : Type u_1} [PartialOrder α] {l₁ l₂ : List α} (hl₁ : l₁.SortedLE) (hl₂ : l₂.SortedLE) (hl₁₂ : l₁.Perm l₂) : l₁ = l₂

theorem List.Perm.eq_of_sortedGE {α : Type u_1} [PartialOrder α] {l₁ l₂ : List α} (hl₁ : l₁.SortedGE) (hl₂ : l₂.SortedGE) (hl₁₂ : l₁.Perm l₂) : l₁ = l₂

theorem List.Subset.antisymm_of_sortedLT {α : Type u_1} [PartialOrder α] {l₁ l₂ : List α} (hl₁₂ : l₁ ⊆ l₂) (hl₁₂' : l₂ ⊆ l₁) (h₁ : l₁.SortedLT) (h₂ : l₂.SortedLT) : l₁ = l₂

theorem List.Subset.antisymm_of_sortedGT {α : Type u_1} [PartialOrder α] {l₁ l₂ : List α} (hl₁₂ : l₁ ⊆ l₂) (hl₁₂' : l₂ ⊆ l₁) (h₁ : l₁.SortedGT) (h₂ : l₂.SortedGT) : l₁ = l₂

theorem List.SortedLT.eq_of_mem_iff {α : Type u_1} [PartialOrder α] {l₁ l₂ : List α} (h₁ : l₁.SortedLT) (h₂ : l₂.SortedLT) (h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂) : l₁ = l₂

theorem List.SortedGT.eq_of_mem_iff {α : Type u_1} [PartialOrder α] {l₁ l₂ : List α} (h₁ : l₁.SortedGT) (h₂ : l₂.SortedGT) (h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂) : l₁ = l₂

theorem List.Perm.eq_reverse_of_sortedLE_of_sortedGE {α : Type u_1} [PartialOrder α] {l₁ l₂ : List α} (hp : l₁.Perm l₂) (hl₁ : l₁.SortedLE) (hl₂ : l₂.SortedGE) : l₁ = l₂.reverse

theorem List.SortedLT.eq_reverse_of_mem_iff_of_sortedGT {α : Type u_1} [PartialOrder α] {l₁ l₂ : List α} (h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂) (hl₁ : l₁.SortedLT) (hl₂ : l₂.SortedGT) : l₁ = l₂.reverse

theorem List.SortedGT.eq_reverse_of_mem_iff_of_sortedLT {α : Type u_1} [PartialOrder α] {l₁ l₂ : List α} (h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂) (hl₁ : l₁.SortedGT) (hl₂ : l₂.SortedLT) : l₁ = l₂.reverse

theorem List.sublist_of_subperm_of_sortedLE {α : Type u_1} [PartialOrder α] {l₁ l₂ : List α} (hp : l₁.Subperm l₂) (hl₁ : l₁.SortedLE) (hl₂ : l₂.SortedLE) : l₁.Sublist l₂

theorem List.sublist_of_subperm_of_sortedGE {α : Type u_1} [PartialOrder α] {l₁ l₂ : List α} (hp : l₁.Subperm l₂) (hl₁ : l₁.SortedGE) (hl₂ : l₂.SortedGE) : l₁.Sublist l₂

theorem List.sortedLE_mergeSort {α : Type u_1} {l : List α} [LinearOrder α] : (l.mergeSort fun (x1 x2 : α) => decide (x1 ≤ x2)).SortedLE

theorem List.sortedGE_mergeSort {α : Type u_1} {l : List α} [LinearOrder α] : (l.mergeSort fun (x1 x2 : α) => decide (x1 ≥ x2)).SortedGE

theorem List.sortedLE_insertionSort {α : Type u_1} {l : List α} [LinearOrder α] : (insertionSort (fun (x1 x2 : α) => x1 ≤ x2) l).SortedLE

theorem List.sortedGE_insertionSort {α : Type u_1} {l : List α} [LinearOrder α] : (insertionSort (fun (x1 x2 : α) => x1 ≥ x2) l).SortedGE

@[simp]

theorem List.SortedLT.getElem_le_getElem_iff {α : Type u_1} {l : List α} [LinearOrder α] (hl : l.SortedLT) {i j : ℕ} {hi : i < l.length} {hj : j < l.length} : l[i] ≤ l[j] ↔ i ≤ j

@[simp]

theorem List.SortedGT.getElem_le_getElem_iff {α : Type u_1} {l : List α} [LinearOrder α] (hl : l.SortedGT) {i j : ℕ} {hi : i < l.length} {hj : j < l.length} : l[i] ≤ l[j] ↔ j ≤ i

@[simp]

theorem List.SortedLT.getElem_lt_getElem_iff {α : Type u_1} {l : List α} [LinearOrder α] (hl : l.SortedLT) {i j : ℕ} {hi : i < l.length} {hj : j < l.length} : l[i] < l[j] ↔ i < j

@[simp]

theorem List.SortedGT.getElem_lt_getElem_iff {α : Type u_1} {l : List α} [LinearOrder α] (hl : l.SortedGT) {i j : ℕ} {hi : i < l.length} {hj : j < l.length} : l[i] < l[j] ↔ j < i

@[simp]

theorem RelEmbedding.pairwise_listMap {α : Type u_1} {β : Type u_2} {ra : α → α → Prop} {rb : β → β → Prop} (e : ra ↪r rb) {l : List α} : List.Pairwise rb (List.map (⇑e) l) ↔ List.Pairwise ra l

@[simp]

theorem RelEmbedding.pairwise_swap_listMap {α : Type u_1} {β : Type u_2} {ra : α → α → Prop} {rb : β → β → Prop} (e : ra ↪r rb) {l : List α} : List.Pairwise (Function.swap rb) (List.map (⇑e) l) ↔ List.Pairwise (Function.swap ra) l

@[simp]

theorem RelIso.pairwise_listMap {α : Type u_1} {β : Type u_2} {ra : α → α → Prop} {rb : β → β → Prop} (e : ra ≃r rb) {l : List α} : List.Pairwise rb (List.map (⇑e) l) ↔ List.Pairwise ra l

@[simp]

theorem RelIso.pairwise_swap_listMap {α : Type u_1} {β : Type u_2} {ra : α → α → Prop} {rb : β → β → Prop} (e : ra ≃r rb) {l : List α} : List.Pairwise (Function.swap rb) (List.map (⇑e) l) ↔ List.Pairwise (Function.swap ra) l

@[simp]

theorem OrderEmbedding.sortedLE_listMap {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) {l : List α} : (List.map (⇑e) l).SortedLE ↔ l.SortedLE

@[simp]

theorem OrderEmbedding.sortedLT_listMap {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) {l : List α} : (List.map (⇑e) l).SortedLT ↔ l.SortedLT

@[simp]

theorem OrderEmbedding.sortedGE_listMap {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) {l : List α} : (List.map (⇑e) l).SortedGE ↔ l.SortedGE

@[simp]

theorem OrderEmbedding.sortedGT_listMap {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) {l : List α} : (List.map (⇑e) l).SortedGT ↔ l.SortedGT

@[simp]

theorem OrderIso.sortedLT_listMap {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) {l : List α} : (List.map (⇑e) l).SortedLT ↔ l.SortedLT

@[simp]

theorem OrderIso.sortedGT_listMap {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) {l : List α} : (List.map (⇑e) l).SortedGT ↔ l.SortedGT

theorem StrictMono.sortedLE_listMap {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : α → β} {l : List α} (hf : StrictMono f) : (List.map f l).SortedLE ↔ l.SortedLE

theorem StrictMono.sortedGE_listMap {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : α → β} {l : List α} (hf : StrictMono f) : (List.map f l).SortedGE ↔ l.SortedGE

theorem StrictMono.sortedLT_listMap {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : α → β} {l : List α} (hf : StrictMono f) : (List.map f l).SortedLT ↔ l.SortedLT

theorem StrictMono.sortedGT_listMap {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : α → β} {l : List α} (hf : StrictMono f) : (List.map f l).SortedGT ↔ l.SortedGT

theorem StrictAnti.sortedLE_listMap {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : α → β} {l : List α} (hf : StrictAnti f) : (List.map f l).SortedLE ↔ l.SortedGE

theorem StrictAnti.sortedGE_listMap {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : α → β} {l : List α} (hf : StrictAnti f) : (List.map f l).SortedGE ↔ l.SortedLE

theorem StrictAnti.sortedLT_listMap {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : α → β} {l : List α} (hf : StrictAnti f) : (List.map f l).SortedLT ↔ l.SortedGT

theorem StrictAnti.sortedGT_listMap {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : α → β} {l : List α} (hf : StrictAnti f) : (List.map f l).SortedGT ↔ l.SortedLT