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 n
Tuple.monotone_sort
:f ∘ Tuple.sort f
isMonotone
graph f
produces the finset of pairs (f i, i)
equipped with the lexicographic order.
Equations
- Tuple.graph f = Finset.image (fun (i : Fin n) => (f i, i)) Finset.univ
Instances For
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 = (↑p).1
Instances For
graphEquiv₁ f
is the natural equivalence between Fin n
and graph f
,
mapping i
to (f i, i)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
graphEquiv₂ f
is an equivalence between Fin n
and graph f
that respects the order.
Equations
- Tuple.graphEquiv₂ f = Finset.orderIsoOfFin (Tuple.graph f) (_ : (Tuple.graph f).card = n)
Instances For
sort f
is the permutation that orders Fin n
according to the order of the outputs of f
.
Equations
- Tuple.sort f = (Tuple.graphEquiv₂ f).trans (Tuple.graphEquiv₁ f).symm
Instances For
If f₀ ≤ f₁ ≤ f₂ ≤ ⋯
is a sorted m
-tuple of elements of α
, then for any j : Fin m
and
a : α
we have j < #{i | fᵢ ≤ a}
iff fⱼ ≤ a
.
If two permutations of a tuple f
are both monotone, then they are equal.
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).
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.
The permutation that sorts f
is the identity if and only if f
is monotone.
A permutation of a tuple f
is f
sorted if and only if it is monotone.
The sorted versions of a tuple f
and of any permutation of f
agree.
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.
If the tuple f
is not the same as f ∘ sort f
, then f
has a pair of strictly decreasing
entries.