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

def Finset.Colex (α : Type u_2) : Type u_2

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

instance instInhabitedColex {α : Type u_1} : Inhabited (Finset.Colex α)

def Finset.toColex {α : Type u_2} (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.

@[simp]

theorem Colex.eq_iff {α : Type u_1} (A : Finset α) (B : Finset α) : Finset.toColex A = Finset.toColex B ↔ A = B

instance Colex.instLT {α : Type u_1} [LT α] : 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).

instance Colex.instLE {α : Type u_1} [LT α] : LE (Finset.Colex α)

We can define (≤) in the obvious way.

theorem Colex.lt_def {α : Type u_1} [LT α] (A : Finset α) (B : Finset α) : Finset.toColex A < Finset.toColex B ↔ ∃ k, (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B

theorem Colex.le_def {α : Type u_1} [LT α] (A : Finset α) (B : Finset α) : Finset.toColex A ≤ Finset.toColex B ↔ Finset.toColex A < Finset.toColex B ∨ A = B

theorem Nat.sum_two_pow_lt {k : ℕ} {A : Finset ℕ} (h₁ : ∀ {x : ℕ}, x ∈ A → x < k) : Finset.sum A (Nat.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} [LinearOrder α] [DecidableEq β] [Preorder β] {f : α → β} (h₁ : StrictMono f) (A : Finset α) (B : Finset α) : Finset.toColex (Finset.image f A) < Finset.toColex (Finset.image f B) ↔ Finset.toColex A < Finset.toColex B

Strictly monotone functions preserve the colex ordering.

@[simp]

theorem Colex.hom_fin_lt_iff {n : ℕ} (A : Finset (Fin n)) (B : Finset (Fin n)) : Finset.toColex (Finset.image (fun i => ↑i) A) < Finset.toColex (Finset.image (fun i => ↑i) B) ↔ Finset.toColex A < Finset.toColex B

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

instance Colex.instIsIrreflColexLtInstLT {α : Type u_1} [LT α] : IsIrrefl (Finset.Colex α) fun x x_1 => x < x_1

theorem Colex.lt_trans {α : Type u_1} [LinearOrder α] {a : Finset.Colex α} {b : Finset.Colex α} {c : Finset.Colex α} : a < b → b < c → a < c

theorem Colex.le_trans {α : Type u_1} [LinearOrder α] (a : Finset.Colex α) (b : Finset.Colex α) (c : Finset.Colex α) : a ≤ b → b ≤ c → a ≤ c

instance Colex.instIsTransColexLtInstLTToLTToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLattice {α : Type u_1} [LinearOrder α] : IsTrans (Finset.Colex α) fun x x_1 => x < x_1

theorem Colex.lt_trichotomy {α : Type u_1} [LinearOrder α] (A : Finset.Colex α) (B : Finset.Colex α) : A < B ∨ A = B ∨ B < A

instance Colex.instIsTrichotomousColexLtInstLTToLTToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLattice {α : Type u_1} [LinearOrder α] : IsTrichotomous (Finset.Colex α) fun x x_1 => x < x_1

instance Colex.decidableLt {α : Type u_1} [LinearOrder α] {A : Finset.Colex α} {B : Finset.Colex α} : Decidable (A < B)

instance Colex.instLinearOrderColex {α : Type u_1} [LinearOrder α] : LinearOrder (Finset.Colex α)

theorem Colex.hom_le_iff {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} (h₁ : StrictMono f) (A : Finset α) (B : Finset α) : Finset.toColex (Finset.image f A) ≤ Finset.toColex (Finset.image f B) ↔ Finset.toColex A ≤ Finset.toColex B

Strictly monotone functions preserve the colex ordering.

@[simp]

theorem Colex.hom_fin_le_iff {n : ℕ} (A : Finset (Fin n)) (B : Finset (Fin n)) : Finset.toColex (Finset.image (fun i => ↑i) A) ≤ Finset.toColex (Finset.image (fun i => ↑i) B) ↔ Finset.toColex A ≤ Finset.toColex B

A special case of hom_le_iff which is sometimes useful.

theorem Colex.forall_lt_of_colex_lt_of_forall_lt {α : Type u_1} [LinearOrder α] {A : Finset α} {B : Finset α} (t : α) (h₁ : Finset.toColex A < Finset.toColex B) (h₂ : ∀ (x : α), x ∈ B → x < t) (x : α) : 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} [LinearOrder α] {r : α} {s : Finset α} : Finset.toColex s < Finset.toColex {r} ↔ ∀ (x : α), x ∈ s → x < r

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

theorem Colex.mem_le_of_singleton_le {α : Type u_1} [LinearOrder α] {r : α} {s : Finset α} : Finset.toColex {r} ≤ Finset.toColex s ↔ ∃ x, 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} [LinearOrder α] {r : α} {s : α} : Finset.toColex {r} < Finset.toColex {s} ↔ r < s

Colex is an extension of the base ordering on α.

theorem Colex.singleton_le_iff_le {α : Type u_1} [LinearOrder α] {r : α} {s : α} : Finset.toColex {r} ≤ Finset.toColex {s} ↔ r ≤ s

Colex is an extension of the base ordering on α.

@[simp]

theorem Colex.sdiff_lt_sdiff_iff_lt {α : Type u_1} [LT α] [DecidableEq α] (A : Finset α) (B : Finset α) : Finset.toColex (A \ B) < Finset.toColex (B \ A) ↔ Finset.toColex A < Finset.toColex B

Colex doesn't care if you remove the other set

@[simp]

theorem Colex.sdiff_le_sdiff_iff_le {α : Type u_1} [LinearOrder α] (A : Finset α) (B : Finset α) : Finset.toColex (A \ B) ≤ Finset.toColex (B \ A) ↔ Finset.toColex A ≤ Finset.toColex B

Colex doesn't care if you remove the other set

theorem Colex.empty_toColex_lt {α : Type u_1} [LinearOrder α] {A : Finset α} (hA : Finset.Nonempty A) : Finset.toColex ∅ < Finset.toColex A

theorem Colex.colex_lt_of_ssubset {α : Type u_1} [LinearOrder α] {A : Finset α} {B : Finset α} (h : A ⊂ B) : Finset.toColex A < Finset.toColex 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_toColex_le {α : Type u_1} [LinearOrder α] {A : Finset α} : Finset.toColex ∅ ≤ Finset.toColex A

theorem Colex.colex_le_of_subset {α : Type u_1} [LinearOrder α] {A : Finset α} {B : Finset α} (h : A ⊆ B) : Finset.toColex A ≤ Finset.toColex B

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

@[simp]

theorem Colex.toColexRelHom_apply {α : Type u_1} [LinearOrder α] (s : Finset α) : ↑Colex.toColexRelHom s = Finset.toColex s

def Colex.toColexRelHom {α : Type u_1} [LinearOrder α] : (fun x x_1 => x ⊆ x_1) →r fun x x_1 => x ≤ x_1

The function from finsets to finsets with the colex order is a relation homomorphism.

instance Colex.instOrderBotColexInstLEToLTToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLattice {α : Type u_1} [LinearOrder α] : OrderBot (Finset.Colex α)

instance Colex.instOrderTopColexInstLEToLTToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLattice {α : Type u_1} [LinearOrder α] [Fintype α] : OrderTop (Finset.Colex α)

instance Colex.instLatticeColex {α : Type u_1} [LinearOrder α] : Lattice (Finset.Colex α)

instance Colex.instBoundedOrderColexInstLEToLTToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLattice {α : Type u_1} [LinearOrder α] [Fintype α] : BoundedOrder (Finset.Colex α)

theorem Colex.sum_two_pow_lt_iff_lt (A : Finset ℕ) (B : Finset ℕ) : ((Finset.sum A fun i => 2 ^ i) < Finset.sum B fun i => 2 ^ i) ↔ Finset.toColex A < Finset.toColex B

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

theorem Colex.sum_two_pow_le_iff_lt (A : Finset ℕ) (B : Finset ℕ) : ((Finset.sum A fun i => 2 ^ i) ≤ Finset.sum B fun i => 2 ^ i) ↔ Finset.toColex A ≤ Finset.toColex B

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