Documentation

Mathlib.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 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 #

See also #

Related files are:

Tags #

colex, colexicographic, binary

References #

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.

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

    Instances For
      @[simp]
      theorem Colex.eq_iff {α : Type u_1} (A : Finset α) (B : Finset α) :
      instance Colex.instLT {α : Type u_1} [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).

      instance Colex.instLE {α : Type u_1} [LT α] :

      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 Nat.sum_two_pow_lt {k : } {A : Finset } (h₁ : ∀ {x : }, x Ax < 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 α) :

      Strictly monotone functions preserve the colex ordering.

      @[simp]
      theorem Colex.hom_fin_lt_iff {n : } (A : Finset (Fin n)) (B : Finset (Fin n)) :

      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 < bb < ca < c
      theorem Colex.le_trans {α : Type u_1} [LinearOrder α] (a : Finset.Colex α) (b : Finset.Colex α) (c : Finset.Colex α) :
      a bb ca c
      theorem Colex.lt_trichotomy {α : Type u_1} [LinearOrder α] (A : Finset.Colex α) (B : Finset.Colex α) :
      A < B A = B B < A
      instance Colex.decidableLt {α : Type u_1} [LinearOrder α] {A : Finset.Colex α} {B : Finset.Colex α} :
      Decidable (A < B)
      theorem Colex.hom_le_iff {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : αβ} (h₁ : StrictMono f) (A : Finset α) (B : Finset α) :

      Strictly monotone functions preserve the colex ordering.

      @[simp]
      theorem Colex.hom_fin_le_iff {n : } (A : Finset (Fin n)) (B : Finset (Fin n)) :

      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 Bx < t) (x : α) :
      x Ax < 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 sx < 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 α} :

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

      Colex is an extension of the base ordering on α.

      theorem Colex.singleton_le_iff_le {α : Type u_1} [LinearOrder α] {r : α} {s : α} :

      Colex is an extension of the base ordering on α.

      @[simp]

      Colex doesn't care if you remove the other set

      @[simp]

      Colex doesn't care if you remove the other set

      theorem Colex.colex_lt_of_ssubset {α : Type u_1} [LinearOrder α] {A : Finset α} {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.

      theorem Colex.colex_le_of_subset {α : Type u_1} [LinearOrder α] {A : Finset α} {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.

      @[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.

      Instances For
        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.