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 has_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: 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.binary_iff: colex for α = ℕ is the same as binary (this also proves binary expansions are unique)
Notation
We define < and ≤ to denote colex ordering, useful in particular when
multiple orderings are available in context.
Tags
colex, colexicographic, binary
References
- https://github.com/b-mehta/maths-notes/blob/master/iii/mich/combinatorics.pdf
Todo
Show the subset ordering is a sub-relation of the colex ordering.
We define this type synonym to refer to the colexicographic ordering on finsets rather than the natural subset ordering.
Equations
- finset.colex α = finset α
A convenience constructor to turn a finset α into a finset.colex α, useful in order to
use the colex ordering rather than the subset ordering.
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.
Equations
- finset.colex.has_le = {le := λ (A B : finset.colex α), A < B ∨ A = B}
Strictly monotone functions preserve the colex ordering.
Equations
- colex.finset.colex.linear_order = {le := has_le.le finset.colex.has_le, lt := partial_order.lt._default has_le.le, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := classical.dec_rel has_le.le, decidable_eq := decidable_eq_of_decidable_le (classical.dec_rel has_le.le), decidable_lt := decidable_lt_of_decidable_le (classical.dec_rel has_le.le)}
If {r} is less than or equal to s in the colexicographical sense, then s contains an element greater than or equal to r.
s.to_colex < finset.to_colex {r} iff all elements of s are less than r.
Colex is an extension of the base ordering on α.