mathlib3 documentation

data.fin.tuple.sort

Sorting tuples by their values #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Given an n-tuple f : fin n → α where α is ordered, we may want to turn it into a sorted n-tuple. This file provides an API for doing so, with the sorted n-tuple given by f ∘ tuple.sort f.

Main declarations #

source
def tuple.graph {n : ℕ} {α : Type u_1} [linear_order α] (f : fin n → α) :
finset (α ×ₗ fin n)

graph f produces the finset of pairs (f i, i) equipped with the lexicographic order.

Equations
source
def tuple.graph.proj {n : ℕ} {α : Type u_1} [linear_order α] {f : fin n → α} :
↥(tuple.graph f) → α

Given p : α ×ₗ (fin n) := (f i, i) with p ∈ graph f, graph.proj p is defined to be f i.

Equations
source
@[simp]
theorem tuple.graph.card {n : ℕ} {α : Type u_1} [linear_order α] (f : fin n → α) :
(tuple.graph f).card = n
source
def tuple.graph_equiv₁ {n : ℕ} {α : Type u_1} [linear_order α] (f : fin n → α) :
fin n ≃ ↥(tuple.graph f)

graph_equiv₁ f is the natural equivalence between fin n and graph f, mapping i to (f i, i).

Equations
source
@[simp]
theorem tuple.proj_equiv₁' {n : ℕ} {α : Type u_1} [linear_order α] (f : fin n → α) :
tuple.graph.proj ∘ ⇑(tuple.graph_equiv₁ f) = f
source
def tuple.graph_equiv₂ {n : ℕ} {α : Type u_1} [linear_order α] (f : fin n → α) :
fin n ≃o ↥(tuple.graph f)

graph_equiv₂ f is an equivalence between fin n and graph f that respects the order.

Equations
source
def tuple.sort {n : ℕ} {α : Type u_1} [linear_order α] (f : fin n → α) :
equiv.perm (fin n)

sort f is the permutation that orders fin n according to the order of the outputs of f.

Equations
source
theorem tuple.graph_equiv₂_apply {n : ℕ} {α : Type u_1} [linear_order α] (f : fin n → α) (i : fin n) :
⇑(tuple.graph_equiv₂ f) i = ⇑(tuple.graph_equiv₁ f) (⇑(tuple.sort f) i)
source
theorem tuple.self_comp_sort {n : ℕ} {α : Type u_1} [linear_order α] (f : fin n → α) :
f ∘ ⇑(tuple.sort f) = tuple.graph.proj ∘ ⇑(tuple.graph_equiv₂ f)
source
theorem tuple.monotone_proj {n : ℕ} {α : Type u_1} [linear_order α] (f : fin n → α) :
monotone tuple.graph.proj
source
theorem tuple.monotone_sort {n : ℕ} {α : Type u_1} [linear_order α] (f : fin n → α) :
monotone (f ∘ ⇑(tuple.sort f))
source
theorem tuple.unique_monotone {n : ℕ} {α : Type u_1} [partial_order α] {f : fin n → α} {σ τ : equiv.perm (fin n)} (hfσ : monotone (f ∘ ⇑σ)) (hfτ : monotone (f ∘ ⇑τ)) :
f ∘ ⇑σ = f ∘ ⇑τ

If two permutations of a tuple f are both monotone, then they are equal.

source
theorem tuple.eq_sort_iff' {n : ℕ} {α : Type u_1} [linear_order α] {f : fin n → α} {σ : equiv.perm (fin n)} :
σ = tuple.sort f ↔ strict_mono ⇑(equiv.trans σ (tuple.graph_equiv₁ f))

A permutation σ equals sort f if and only if the map i ↦ (f (σ i), σ i) is strictly monotone (w.r.t. the lexicographic ordering on the target).

source
theorem tuple.eq_sort_iff {n : ℕ} {α : Type u_1} [linear_order α] {f : fin n → α} {σ : equiv.perm (fin n)} :
σ = tuple.sort f ↔ monotone (f ∘ ⇑σ) ∧ ∀ (i j : fin n), i < j → f (⇑σ i) = f (⇑σ j) → ⇑σ i < ⇑σ j

A permutation σ equals sort f if and only if f ∘ σ is monotone and whenever i < j and f (σ i) = f (σ j), then σ i < σ j. This means that sort f is the lexicographically smallest permutation σ such that f ∘ σ is monotone.

source
theorem tuple.sort_eq_refl_iff_monotone {n : ℕ} {α : Type u_1} [linear_order α] {f : fin n → α} :
tuple.sort f = equiv.refl (fin n) ↔ monotone f

The permutation that sorts f is the identity if and only if f is monotone.

source
theorem tuple.comp_sort_eq_comp_iff_monotone {n : ℕ} {α : Type u_1} [linear_order α] {f : fin n → α} {σ : equiv.perm (fin n)} :
f ∘ ⇑σ = f ∘ ⇑(tuple.sort f) ↔ monotone (f ∘ ⇑σ)

A permutation of a tuple f is f sorted if and only if it is monotone.

source
theorem tuple.comp_perm_comp_sort_eq_comp_sort {n : ℕ} {α : Type u_1} [linear_order α] {f : fin n → α} {σ : equiv.perm (fin n)} :
(f ∘ ⇑σ) ∘ ⇑(tuple.sort (f ∘ ⇑σ)) = f ∘ ⇑(tuple.sort f)

The sorted versions of a tuple f and of any permutation of f agree.

source
theorem tuple.antitone_pair_of_not_sorted' {n : ℕ} {α : Type u_1} [linear_order α] {f : fin n → α} {σ : equiv.perm (fin n)} (h : f ∘ ⇑σ ≠ f ∘ ⇑(tuple.sort f)) :
∃ (i j : fin n), i < j ∧ (f ∘ ⇑σ) j < (f ∘ ⇑σ) i

If a permutation f ∘ σ of the tuple f is not the same as f ∘ sort f, then f ∘ σ has a pair of strictly decreasing entries.

source
theorem tuple.antitone_pair_of_not_sorted {n : ℕ} {α : Type u_1} [linear_order α] {f : fin n → α} (h : f ≠ f ∘ ⇑(tuple.sort f)) :
∃ (i j : fin n), i < j ∧ f j < f i

If the tuple f is not the same as f ∘ sort f, then f has a pair of strictly decreasing entries.