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 #

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)

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

@[instance]

def finset.colex.inhabited (α : Type u_1) :

inhabited (finset.colex α)

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

finset.colex α = finset α

def finset.to_colex {α : Type u_1} (s : finset α) :

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.

Equations

s.to_colex = s

@[simp]

theorem colex.eq_iff {α : Type u_1} (A B : finset α) :

A.to_colex = B.to_colex ↔ A = B

@[instance]

def finset.colex.has_lt {α : Type u_1} [has_lt α] :

has_lt (finset.colex α)

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

finset.colex.has_lt = {lt := λ (A B : finset α), ∃ (k : α), (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ k ∉ A ∧ k ∈ B}

@[instance]

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

has_le (finset.colex α)

We can define (≤) in the obvious way.

Equations

finset.colex.has_le = {le := λ (A B : finset.colex α), A < B ∨ A = B}

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 α) :

A.to_colex ≤ B.to_colex ↔ A.to_colex < B.to_colex ∨ A = B

theorem nat.sum_two_pow_lt {k : ℕ} {A : finset ℕ} (h₁ : ∀ {x : ℕ}, x ∈ A → x < 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 α) :

(finset.image f A).to_colex < (finset.image f B).to_colex ↔ A.to_colex < B.to_colex

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]

def colex.has_lt.lt.is_irrefl {α : Type u_1} [has_lt α] :

is_irrefl (finset.colex α) has_lt.lt

theorem colex.lt_trans {α : Type u_1} [linear_order α] {a b c : finset.colex α} :

a < b → b < c → a < c

theorem colex.le_trans {α : Type u_1} [linear_order α] (a b c : finset.colex α) :

a ≤ b → b ≤ c → a ≤ c

@[instance]

def colex.has_lt.lt.is_trans {α : Type u_1} [linear_order α] :

is_trans (finset.colex α) has_lt.lt

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

A < B ∨ A = B ∨ B < A

@[instance]

def colex.has_lt.lt.is_trichotomous {α : Type u_1} [linear_order α] :

is_trichotomous (finset.colex α) has_lt.lt

@[instance]

def colex.decidable_lt {α : Type u_1} [linear_order α] {A B : finset.colex α} :

decidable (A < B)

Equations

colex.decidable_lt = show Π (A B : finset α), decidable (A.to_colex < B.to_colex), from λ (A B : finset α), decidable_of_iff' (∃ (k : α) (H : k ∈ B), (∀ (x : α), x ∈ A ∪ B → k < x → (x ∈ A ↔ x ∈ B)) ∧ k ∉ A) _

@[instance]

def colex.finset.colex.linear_order {α : Type u_1} [linear_order α] :

linear_order (finset.colex α)

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 := _}

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

(finset.image f A).to_colex ≤ (finset.image f B).to_colex ↔ A.to_colex ≤ B.to_colex

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 ∈ B → x < 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 ∈ s → x < 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 : α} :

{r}.to_colex ≤ {s}.to_colex ↔ 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 α) :

(A \ B).to_colex < (B \ A).to_colex ↔ A.to_colex < B.to_colex

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 α) :

(A \ B).to_colex ≤ (B \ A).to_colex ↔ A.to_colex ≤ B.to_colex

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

∅.to_colex < A.to_colex

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

A.to_colex < B.to_colex

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 α} :

∅.to_colex ≤ A.to_colex

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

A.to_colex ≤ B.to_colex

If A ⊆ B, then A ≤ B in the colex order. Note the converse does not hold, as ⊆ is not a linear order.

def colex.to_colex_rel_hom {α : Type u_1} [linear_order α] :

has_subset.subset →r has_le.le

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' := _}

@[simp]

theorem colex.to_colex_rel_hom_apply {α : Type u_1} [linear_order α] (s : finset α) :

⇑colex.to_colex_rel_hom s = s.to_colex

@[instance]

def colex.finset.colex.order_bot {α : Type u_1} [linear_order α] :

order_bot (finset.colex α)

Equations

colex.finset.colex.order_bot = {bot := ∅.to_colex, le := partial_order.le (semilattice_inf.to_partial_order (finset.colex α)), lt := partial_order.lt (semilattice_inf.to_partial_order (finset.colex α)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}

@[instance]

def colex.finset.colex.semilattice_inf_bot {α : Type u_1} [linear_order α] :

semilattice_inf_bot (finset.colex α)

Equations

colex.finset.colex.semilattice_inf_bot = {bot := order_bot.bot colex.finset.colex.order_bot, le := order_bot.le colex.finset.colex.order_bot, lt := order_bot.lt colex.finset.colex.order_bot, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, inf := semilattice_inf.inf (lattice.to_semilattice_inf (finset.colex α)), inf_le_left := _, inf_le_right := _, le_inf := _}

@[instance]

def colex.finset.colex.semilattice_sup_bot {α : Type u_1} [linear_order α] :

semilattice_sup_bot (finset.colex α)

Equations

colex.finset.colex.semilattice_sup_bot = {bot := order_bot.bot colex.finset.colex.order_bot, le := order_bot.le colex.finset.colex.order_bot, lt := order_bot.lt colex.finset.colex.order_bot, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := semilattice_sup.sup (lattice.to_semilattice_sup (finset.colex α)), le_sup_left := _, le_sup_right := _, sup_le := _}

@[instance]

def colex.finset.colex.bounded_lattice {α : Type u_1} [linear_order α] [fintype α] :

bounded_lattice (finset.colex α)

Equations

colex.finset.colex.bounded_lattice = {sup := semilattice_sup.sup (semilattice_sup_bot.to_semilattice_sup (finset.colex α)), le := semilattice_sup.le (semilattice_sup_bot.to_semilattice_sup (finset.colex α)), lt := semilattice_sup.lt (semilattice_sup_bot.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_bot.inf colex.finset.colex.semilattice_inf_bot, inf_le_left := _, inf_le_right := _, le_inf := _, top := finset.univ.to_colex, le_top := _, bot := semilattice_inf_bot.bot colex.finset.colex.semilattice_inf_bot, bot_le := _}

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.