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 #
tuple.sort: givenf : fin n → α, produces a permutation onfin ntuple.monotone_sort:f ∘ tuple.sort fismonotone
graph f produces the finset of pairs (f i, i)
equipped with the lexicographic order.
Equations
- tuple.graph f = finset.image (λ (i : fin n), (f i, i)) finset.univ
Given p : α ×ₗ (fin n) := (f i, i) with p ∈ graph f,
graph.proj p is defined to be f i.
Equations
- tuple.graph.proj = λ (p : ↥(tuple.graph f)), p.val.fst
@[simp]
theorem
tuple.graph.card
{n : ℕ}
{α : Type u_1}
[linear_order α]
(f : fin n → α) :
(tuple.graph f).card = n
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).
@[simp]
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
sort f is the permutation that orders fin n according to the order of the outputs of f.
Equations
- tuple.sort f = (tuple.graph_equiv₂ f).to_equiv.trans (tuple.graph_equiv₁ f).symm
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)
theorem
tuple.monotone_sort
{n : ℕ}
{α : Type u_1}
[linear_order α]
(f : fin n → α) :
monotone (f ∘ ⇑(tuple.sort f))