mathlib documentation

data.fin.tuple.sort

Sorting tuples by their values #

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 #

def tuple.graph {n : } {α : Type u_1} [linear_order α] (f : fin n → α) :

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

Equations
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
@[simp]
theorem tuple.graph.card {n : } {α : Type u_1} [linear_order α] (f : fin n → α) :
def tuple.graph_equiv₁ {n : } {α : Type u_1} [linear_order α] (f : fin n → α) :

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

Equations
@[simp]
theorem tuple.proj_equiv₁' {n : } {α : Type u_1} [linear_order α] (f : fin n → α) :
def tuple.graph_equiv₂ {n : } {α : Type u_1} [linear_order α] (f : fin n → α) :

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

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

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

Equations
theorem tuple.self_comp_sort {n : } {α : Type u_1} [linear_order α] (f : fin n → α) :
theorem tuple.monotone_proj {n : } {α : Type u_1} [linear_order α] (f : fin n → α) :
theorem tuple.monotone_sort {n : } {α : Type u_1} [linear_order α] (f : fin n → α) :