Colex #
We define the colex ordering for finite sets, and give a couple of important lemmas and properties relating to it.
The colex ordering likes to avoid large values - it can be thought of on
Finset ℕ
as the "binary" ordering. That is, order A based on
∑_{i ∈ A} 2^i
.
It's defined here in a slightly more general way, requiring only LT α
in
the definition of colex on Finset α
. In the context of the Kruskal-Katona
theorem, we are interested in particular on how colex behaves for sets of a
fixed size. If the size is 3, colex on ℕ starts
123, 124, 134, 234, 125, 135, 235, 145, 245, 345, ...
Main statements #
Colex.hom_lt_iff
: strictly monotone functions preserve colex- Colex order properties - linearity, decidability and so on.
forall_lt_of_colex_lt_of_forall_lt
: if A < B in colex, and everything in B is < t, then everything in A is < t. This confirms the idea that an enumeration under colex will exhaust all sets using elements < t before allowing t to be included.sum_two_pow_le_iff_lt
: colex for α = ℕ is the same as binary (this also proves binary expansions are unique)
See also #
Related files are:
Data.List.Lex
: Lexicographic order on lists.Data.Pi.Lex
: Lexicographic order on(i : α) → α i
.Data.PSigma.Order
: Lexicographic order onΣ' i, α i
.Data.Sigma.Order
: Lexicographic order onΣ i, α i
.Data.Prod.Lex
: Lexicographic order onα × β
.
Tags #
colex, colexicographic, binary
References #
- https://github.com/b-mehta/maths-notes/blob/master/iii/mich/combinatorics.pdf
We define this type synonym to refer to the colexicographic ordering on finsets rather than the natural subset ordering.
Instances For
A convenience constructor to turn a Finset α
into a Finset.Colex α
, useful in order to
use the colex ordering rather than the subset ordering.
Instances For
A
is less than B
in the colex ordering if the largest thing that's not in both sets is in B.
In other words, max (A ∆ B) ∈ B
(if the maximum exists).
We can define (≤) in the obvious way.
Strictly monotone functions preserve the colex ordering.
A special case of Colex.hom_lt_iff
which is sometimes useful.
Strictly monotone functions preserve the colex ordering.
A special case of hom_le_iff
which is sometimes useful.
If A
is before B
in colex, and everything in B
is small, then everything in A
is small.
s.toColex < {r}.toColex
iff all elements of s
are less than r
.
If {r}
is less than or equal to s in the colexicographical sense,
then s contains an element greater than or equal to r.
Colex is an extension of the base ordering on α.
Colex is an extension of the base ordering on α.
Colex doesn't care if you remove the other set
Colex doesn't care if you remove the other set
If A ⊂ B
, then A
is less than B
in the colex order. Note the converse does not hold, as
⊆
is not a linear order.
If A ⊆ B
, then A ≤ B
in the colex order. Note the converse does not hold, as ⊆
is not a
linear order.
The function from finsets to finsets with the colex order is a relation homomorphism.
Instances For
For subsets of ℕ, we can show that colex is equivalent to binary.
For subsets of ℕ, we can show that colex is equivalent to binary.