Colex #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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_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 #
We define this type synonym to refer to the colexicographic ordering on finsets rather than the natural subset ordering.
Equations
- finset.colex α = finset α
Instances for finset.colex
A convenience constructor to turn a finset α
into a finset.colex α
, useful in order to
use the colex ordering rather than the subset ordering.
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.
A special case of colex.hom_lt_iff
which is sometimes useful.
Equations
- colex.finset.colex.linear_order = {le := has_le.le finset.colex.has_le, lt := has_lt.lt finset.colex.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := λ (A B : finset.colex α), or.decidable, decidable_eq := λ (A B : finset.colex α), finset.has_decidable_eq A B, decidable_lt := λ (A B : finset.colex α), colex.decidable_lt, max := max_default (λ (a b : finset.colex α), or.decidable), max_def := _, min := min_default (λ (a b : finset.colex α), or.decidable), min_def := _}
Strictly monotone functions preserve the colex ordering.
Colex is an extension of the base ordering on α.
Colex is an extension of the base ordering on α.
The function from finsets to finsets with the colex order is a relation homomorphism.
Equations
- colex.to_colex_rel_hom = {to_fun := finset.to_colex α, map_rel' := _}
Equations
- colex.finset.colex.order_top = {top := finset.univ.to_colex, le_top := _}
Equations
- colex.finset.colex.lattice = {sup := semilattice_sup.sup (lattice.to_semilattice_sup (finset.colex α)), le := semilattice_sup.le (lattice.to_semilattice_sup (finset.colex α)), lt := semilattice_sup.lt (lattice.to_semilattice_sup (finset.colex α)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf (lattice.to_semilattice_inf (finset.colex α)), inf_le_left := _, inf_le_right := _, le_inf := _}