mathlib documentation

combinatorics.colex

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 #

Notation #

We define < and to denote colex ordering, useful in particular when multiple orderings are available in context.

Tags #

colex, colexicographic, binary

References #

@[instance]
def finset.colex.inhabited (α : Type u_1) :
def finset.colex (α : Type u_1) :
Type u_1

We define this type synonym to refer to the colexicographic ordering on finsets rather than the natural subset ordering.

Equations
def finset.to_colex {α : Type u_1} (s : 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.

Equations
@[simp]
theorem colex.eq_iff {α : Type u_1} (A B : finset α) :
@[instance]
def finset.colex.has_lt {α : Type u_1} [has_lt α] :

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).

Equations
@[instance]
def finset.colex.has_le {α : Type u_1} [has_lt α] :

We can define (≤) in the obvious way.

Equations
theorem colex.lt_def {α : Type u_1} [has_lt α] (A B : finset α) :
A.to_colex < B.to_colex ∃ (k : α), (∀ {x : α}, k < x(x A x B)) k A k B
theorem colex.le_def {α : Type u_1} [has_lt α] (A B : finset α) :
theorem nat.sum_two_pow_lt {k : } {A : finset } (h₁ : ∀ {x : }, x Ax < k) :
A.sum (pow 2) < 2 ^ k

If everything in A is less than k, we can bound the sum of powers.

theorem colex.hom_lt_iff {α : Type u_1} {β : Type u_2} [linear_order α] [decidable_eq β] [preorder β] {f : α → β} (h₁ : strict_mono f) (A B : finset α) :

Strictly monotone functions preserve the colex ordering.

@[simp]
theorem colex.hom_fin_lt_iff {n : } (A B : finset (fin n)) :
(finset.image (λ (i : fin n), i) A).to_colex < (finset.image (λ (i : fin n), i) B).to_colex A.to_colex < B.to_colex

A special case of colex.hom_lt_iff which is sometimes useful.

@[instance]
theorem colex.lt_trans {α : Type u_1} [linear_order α] {a b c : finset.colex α} :
a < bb < ca < c
theorem colex.le_trans {α : Type u_1} [linear_order α] (a b c : finset.colex α) :
a bb ca c
@[instance]
theorem colex.lt_trichotomy {α : Type u_1} [linear_order α] (A B : finset.colex α) :
A < B A = B B < A
@[instance]
def colex.decidable_lt {α : Type u_1} [linear_order α] {A B : finset.colex α} :
decidable (A < B)
Equations
theorem colex.hom_le_iff {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] {f : α → β} (h₁ : strict_mono f) (A B : finset α) :

Strictly monotone functions preserve the colex ordering.

@[simp]
theorem colex.hom_fin_le_iff {n : } (A B : finset (fin n)) :
(finset.image (λ (i : fin n), i) A).to_colex (finset.image (λ (i : fin n), i) B).to_colex A.to_colex B.to_colex

A special case of colex_hom which is sometimes useful.

theorem colex.forall_lt_of_colex_lt_of_forall_lt {α : Type u_1} [linear_order α] {A B : finset α} (t : α) (h₁ : A.to_colex < B.to_colex) (h₂ : ∀ (x : α), x Bx < t) (x : α) (H : x A) :
x < t

If A is before B in colex, and everything in B is small, then everything in A is small.

theorem colex.lt_singleton_iff_mem_lt {α : Type u_1} [linear_order α] {r : α} {s : finset α} :
s.to_colex < {r}.to_colex ∀ (x : α), x sx < r

s.to_colex < {r}.to_colex iff all elements of s are less than r.

theorem colex.mem_le_of_singleton_le {α : Type u_1} [linear_order α] {r : α} {s : finset α} :
{r}.to_colex s.to_colex ∃ (x : α) (H : x s), r x

If {r} is less than or equal to s in the colexicographical sense, then s contains an element greater than or equal to r.

theorem colex.singleton_lt_iff_lt {α : Type u_1} [linear_order α] {r s : α} :
{r}.to_colex < {s}.to_colex r < s

Colex is an extension of the base ordering on α.

theorem colex.singleton_le_iff_le {α : Type u_1} [linear_order α] {r s : α} :

Colex is an extension of the base ordering on α.

@[simp]
theorem colex.sdiff_lt_sdiff_iff_lt {α : Type u_1} [has_lt α] [decidable_eq α] (A B : finset α) :

Colex doesn't care if you remove the other set

@[simp]
theorem colex.sdiff_le_sdiff_iff_le {α : Type u_1} [linear_order α] (A B : finset α) :

Colex doesn't care if you remove the other set

theorem colex.empty_to_colex_lt {α : Type u_1} [linear_order α] {A : finset α} (hA : A.nonempty) :
theorem colex.colex_lt_of_ssubset {α : Type u_1} [linear_order α] {A B : finset α} (h : A B) :

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.

@[simp]
theorem colex.empty_to_colex_le {α : Type u_1} [linear_order α] {A : finset α} :
theorem colex.colex_le_of_subset {α : Type u_1} [linear_order α] {A B : finset α} (h : A B) :

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.

Equations
@[simp]
theorem colex.sum_two_pow_lt_iff_lt (A B : finset ) :
∑ (i : ) in A, 2 ^ i < ∑ (i : ) in B, 2 ^ i A.to_colex < B.to_colex

For subsets of ℕ, we can show that colex is equivalent to binary.

theorem colex.sum_two_pow_le_iff_lt (A B : finset ) :
∑ (i : ) in A, 2 ^ i ∑ (i : ) in B, 2 ^ i A.to_colex B.to_colex

For subsets of ℕ, we can show that colex is equivalent to binary.