Sorting finsets

Sorting the finset {a, b} of two distinct elements with r a b gives the list [a, b], and sorting s.erase a gives the sorted list of s with a erased.

For a map f that is monotone on a finset s of a linear order, the points of s sorted in increasing order are the concatenation, over the values y of f on s in increasing order, of the sorted fibres {x ∈ s | f x = y}. Consequently the ordered product of a word along s is the ordered product, over the values of f on s, of the ordered products along the fibres.

Consecutive entries of the sorted list of s are the pairs of positions of s with no position of s strictly between them, so a chain condition on the sorted list is a condition on such adjacent pairs.

The m-th element of a finset s in increasing order, s.orderEmbOfFin h m, has exactly m elements of s below it.

Mapping the sorted list of s along an embedding that is strictly antitone on s gives the sorted list of the image in reversed order; in particular, sorting the points of a finset of Fin n moved along the reversal Fin.rev reverses the list of their images.

Moving the points of a finset B of Fin n along the rotation finRotate n (i ↦ i + 1, the last position going to 0) commutes with sorting up to a cyclic rotation of the list.

The i-th smallest element of s has exactly i elements of s below it.

Removing the position of i from the increasing enumeration of s gives the increasing enumeration of s.erase i.

Every nonempty finset can be listed by a sequence strictly increasing on a finite initial segment (Finset.exists_strictMonoOn_Iic_surj).

If every element of I is at most s ≤ t, the sequence ⊥, the elements of I in increasing order, s, then constantly t, is monotone in ℕ, Finset.monotone_bot_orderEmbOfFin_snoc.

The support-enlargement and adjacent-swap ordered-product lemmas are adapted from Mei/Algebra/BigOperators/Group/Finset/Ordered.lean in yuma-mizuno-lean/Mei, commit 3d2e9c869ee44c41ae9c7b5c6e2042898430d0ca (Apache 2.0), originally authored by Codex.

theorem Finset.sort_pair {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [Std.Antisymm r] [Std.Total r] [DecidableEq α] {a b : α} (hab : r a b) (hne : a ≠ b) : {a, b}.sort r = [a, b]

Sorting a two-element finset {a, b} with r a b lists a before b.

theorem Finset.sort_erase {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [Std.Antisymm r] [Std.Total r] [DecidableEq α] (s : Finset α) (a : α) : (s.erase a).sort r = (s.sort r).erase a

Sorting s.erase a erases a from the sorted list of s.

theorem Finset.exists_strictMonoOn_Iic_surj {α : Type u_2} [LinearOrder α] (d : Finset α) (hd : d.Nonempty) : ∃ (n : ℕ) (τ : ℕ → α), StrictMonoOn τ (Set.Iic n) ∧ (∀ j ≤ n, τ j ∈ d) ∧ ∀ x ∈ d, ∃ j ≤ n, τ j = x

A nonempty finset in a linear order can be listed by a sequence strictly increasing on Set.Iic n, with all entries on that segment in the finset and every element reached there.

theorem Finset.collapse_adjacent_spec {α : Type u_2} [LinearOrder α] {s : Finset α} {i j : α} (hi : i ∈ s) (hj : j ∈ s) (hij : i < j) (hadj : ∀ z ∈ s, z ≤ i ∨ j ≤ z) : MonotoneOn (fun (z : α) => if z = j then i else z) ↑s ∧ (∀ {u v : α}, ((if u = j then i else u) = if v = j then i else v) → u ≠ v → (u = i ∨ u = j) ∧ (v = i ∨ v = j)) ∧ (image (fun (z : α) => if z = j then i else z) s).card < s.card

Collapsing j onto its predecessor i in s is monotone on s, identifies only i and j, and strictly decreases the cardinality of the image of s.

theorem Finset.flatten_map_sort_filter_eq_sort {α : Type u_2} {β : Type u_3} [LinearOrder α] [LinearOrder β] {s : Finset α} {f : α → β} (hf : MonotoneOn f ↑s) : (List.map (fun (y : β) => {x ∈ s | f x = y}.sort fun (a b : α) => a ≤ b) ((image f s).sort fun (a b : β) => a ≤ b)).flatten = s.sort fun (a b : α) => a ≤ b

For a map f that is monotone on s, listing the values of f on s in increasing order and replacing each value y by the increasing list of the points of s over y lists s in increasing order.

theorem Finset.prod_map_sort_eq_prod_map_sort_image {α : Type u_2} {β : Type u_3} [LinearOrder α] [LinearOrder β] {s : Finset α} {f : α → β} {M : Type u_4} [Monoid M] (hf : MonotoneOn f ↑s) (a : α → M) : (List.map a (s.sort fun (a b : α) => a ≤ b)).prod = (List.map (fun (y : β) => (List.map a ({x ∈ s | f x = y}.sort fun (a b : α) => a ≤ b)).prod) ((image f s).sort fun (a b : β) => a ≤ b)).prod

For a map f that is monotone on s, the product of a word a along s in increasing order is the product, over the values y of f on s in increasing order, of the products of a along the fibres {x ∈ s | f x = y} in increasing order.

theorem Finset.prod_map_sort_subset {ι : Type u_4} {M : Type u_5} [LinearOrder ι] [Monoid M] {s t : Finset ι} (hst : s ⊆ t) (f : ι → M) (hf : ∀ i ∈ t, i ∉ s → f i = 1) : (List.map f (s.sort fun (a b : ι) => a ≤ b)).prod = (List.map f (t.sort fun (a b : ι) => a ≤ b)).prod

Enlarging an ordered index set by identity factors preserves the product.

theorem Finset.prod_map_sort_eq_of_ne_one {ι : Type u_4} {M : Type u_5} [LinearOrder ι] [Monoid M] (s t : Finset ι) (f : ι → M) (h : ∀ (i : ι), f i ≠ 1 → (i ∈ s ↔ i ∈ t)) : (List.map f (s.sort fun (a b : ι) => a ≤ b)).prod = (List.map f (t.sort fun (a b : ι) => a ≤ b)).prod

Sorted products agree when their index sets agree wherever the factor is not one.

theorem Finset.prod_map_sort_swap {ι : Type u_4} {M : Type u_5} [LinearOrder ι] [Monoid M] (s : Finset ι) (f : ι → M) {a b : ι} (hab : a < b) (ha : a ∈ s) (hb : b ∈ s) (hgap : ∀ i ∈ s, ¬(a < i ∧ i < b)) (hcomm : Commute (f a) (f b)) : (List.map (fun (i : ι) => f ((Equiv.swap a b) i)) (s.sort fun (a b : ι) => a ≤ b)).prod = (List.map f (s.sort fun (a b : ι) => a ≤ b)).prod

Swapping two consecutive indices in a finite increasing product preserves it when their factors commute.

theorem Finset.isChain_map_sort_iff {α : Type u_2} [LinearOrder α] {s : Finset α} {γ : Type u_4} {r : γ → γ → Prop} {g : α → γ} : List.IsChain r (List.map g (s.sort fun (a b : α) => a ≤ b)) ↔ ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ≤ x ∨ y ≤ z) → r (g x) (g y)

A relation holds between the images of consecutive entries of s sorted in increasing order exactly when it holds between the images of any two positions x < y of s with no position of s strictly between them.

theorem StrictAntiOn.map_finsetSort {α : Type u_2} {β : Type u_3} [LinearOrder α] [LinearOrder β] {s : Finset α} {e : α ↪ β} (he : StrictAntiOn ⇑e ↑s) : List.map (⇑e) (s.sort fun (a b : α) => a ≤ b) = ((Finset.map e s).sort fun (a b : β) => a ≤ b).reverse

For an embedding e that is strictly antitone on s, mapping the increasing list of s along e gives the decreasing list of the image of s, the reverse of its increasing list.

theorem Finset.card_filter_lt_orderEmbOfFin {α : Type u_2} [LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k) (m : Fin k) : {j ∈ s | j < (s.orderEmbOfFin h) m}.card = ↑m

The m-th element of s in increasing order has exactly m elements of s below it.

theorem Finset.sort_map_revPerm {n : ℕ} (B : Finset (Fin n)) : ((map (Equiv.toEmbedding Fin.revPerm) B).sort fun (a b : Fin n) => a ≤ b) = (List.map Fin.rev (B.sort fun (a b : Fin n) => a ≤ b)).reverse

Sorting the points of a finset B of Fin n moved along the reversal Fin.revPerm lists the images under Fin.rev of the sorted points of B in reversed order.

theorem Finset.isRotated_sort_map_finRotate {n : ℕ} (B : Finset (Fin n)) : List.map (⇑(finRotate n)) (B.sort fun (a b : Fin n) => a ≤ b) ~r (map (Equiv.toEmbedding (finRotate n)) B).sort fun (a b : Fin n) => a ≤ b

Sorting a finset B of Fin n and then moving its points along finRotate n gives a cyclic rotation of the sorted list of the moved points: the order is unchanged except that the last position, which moves to 0, goes from the end of the list to its front.

theorem Finset.removeNth_orderEmbOfFin_symm_eq {I : Type u_4} [LinearOrder I] (i : I) (s : Finset I) (hi : i ∈ s) (hsCard : s.card = (s.erase i).card + 1) : (((s.orderIsoOfFin hsCard).symm ⟨i, hi⟩).removeNth fun (j : Fin ((s.erase i).card + 1)) => (s.orderEmbOfFin hsCard) j) = ⇑((s.erase i).orderEmbOfFin ⋯)

Removing the position of i from the increasing enumeration of s gives the increasing enumeration of s.erase i.

theorem Finset.monotone_bot_orderEmbOfFin_snoc {T : Type u_2} [LinearOrder T] [OrderBot T] (I : Finset T) {s t : T} (hI : ∀ i ∈ I, i ≤ s) (hst : s ≤ t) : Monotone fun (n : ℕ) => if h : n = 0 then ⊥ else if h_1 : n ≤ I.card then (I.orderEmbOfFin ⋯) ⟨n - 1, ⋯⟩ else if n = I.card + 1 then s else t

If every element of I is at most s and s ≤ t, then the sequence ⊥, the elements of I in increasing order, s, then constantly t (from index I.card + 2 on), is monotone in ℕ.