Colexigraphic order #

We define the colex order for finite sets, and give a couple of important lemmas and properties relating to it.

The colex ordering likes to avoid large values: If the biggest element of t is bigger than all elements of s, then s < t.

In the special case of ℕ, it can be thought of as the "binary" ordering. That is, order s based on $∑_{i ∈ s} 2^i$. It's defined here on Finset α for any linear order α.

In the context of the Kruskal-Katona theorem, we are interested in how colex behaves for sets of a fixed size. For example, for size 3, the colex order on ℕ starts 012, 013, 023, 123, 014, 024, 124, 034, 134, 234, ...

Main statements #

• Colex order properties - linearity, decidability and so on.
• Finset.Colex.forall_lt_mono: if s < t in colex, and everything in t is < a, then everything in s is < a. This confirms the idea that an enumeration under colex will exhaust all sets using elements < a before allowing a to be included.
• Finset.toColex_image_le_toColex_image: Strictly monotone functions preserve colex.
• Finset.geomSum_le_geomSum_iff_toColex_le_toColex: Colex for α = ℕ is the same as binary. This also proves binary expansions are unique.

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 α × β.

TODO #

• Generalise Colex.initSeg so that it applies to ℕ.

References #

• https://github.com/b-mehta/maths-notes/blob/master/iii/mich/combinatorics.pdf

Tags #

colex, colexicographic, binary

theorem Finset.Colex.ext {α : Type u_3} (x : ) (y : ) (ofColex : x.ofColex = y.ofColex) :
x = y
theorem Finset.Colex.ext_iff {α : Type u_3} (x : ) (y : ) :
x = y x.ofColex = y.ofColex
structure Finset.Colex (α : Type u_3) :
Type u_3

Type synonym of Finset α equipped with the colexicographic order rather than the inclusion order.

• toColex :: (
• ofColex :

ofColex is the "identity" function between Finset.Colex α and Finset α.

• )
Instances For
instance Finset.instInhabitedColex {α : Type u_1} :
Equations
• Finset.instInhabitedColex = { default := { ofColex := } }
@[simp]
theorem Finset.toColex_ofColex {α : Type u_1} (s : ) :
{ ofColex := s.ofColex } = s
theorem Finset.ofColex_toColex {α : Type u_1} (s : ) :
{ ofColex := s }.ofColex = s
theorem Finset.toColex_inj {α : Type u_1} {s : } {t : } :
{ ofColex := s } = { ofColex := t } s = t
@[simp]
theorem Finset.ofColex_inj {α : Type u_1} {s : } {t : } :
s.ofColex = t.ofColex s = t
theorem Finset.toColex_ne_toColex {α : Type u_1} {s : } {t : } :
{ ofColex := s } { ofColex := t } s t
theorem Finset.ofColex_ne_ofColex {α : Type u_1} {s : } {t : } :
s.ofColex t.ofColex s t
theorem Finset.toColex_injective {α : Type u_1} :
Function.Injective Finset.Colex.toColex
theorem Finset.ofColex_injective {α : Type u_1} :
Function.Injective Finset.Colex.ofColex
instance Finset.Colex.instLE {α : Type u_1} [] :
LE ()
Equations
• Finset.Colex.instLE = { le := fun (s t : ) => ∀ ⦃a : α⦄, a s.ofColexat.ofColexbt.ofColex, bs.ofColex a b }
instance Finset.Colex.instPartialOrder {α : Type u_1} [] :
Equations
• Finset.Colex.instPartialOrder =
theorem Finset.Colex.le_def {α : Type u_1} [] {s : } {t : } :
s t ∀ ⦃a : α⦄, a s.ofColexat.ofColexbt.ofColex, bs.ofColex a b
theorem Finset.Colex.toColex_le_toColex {α : Type u_1} [] {s : } {t : } :
{ ofColex := s } { ofColex := t } ∀ ⦃a : α⦄, a satbt, bs a b
theorem Finset.Colex.toColex_lt_toColex {α : Type u_1} [] {s : } {t : } :
{ ofColex := s } < { ofColex := t } s t ∀ ⦃a : α⦄, a satbt, bs a b
theorem Finset.Colex.toColex_mono {α : Type u_1} [] :
Monotone Finset.Colex.toColex

If s ⊆ t, then s ≤ t in the colex order. Note the converse does not hold, as inclusion does not form a linear order.

theorem Finset.Colex.toColex_strictMono {α : Type u_1} [] :
StrictMono Finset.Colex.toColex

If s ⊂ t, then s < t in the colex order. Note the converse does not hold, as inclusion does not form a linear order.

theorem Finset.Colex.toColex_le_toColex_of_subset {α : Type u_1} [] {s : } {t : } (h : s t) :
{ ofColex := s } { ofColex := t }

If s ⊆ t, then s ≤ t in the colex order. Note the converse does not hold, as inclusion does not form a linear order.

theorem Finset.Colex.toColex_lt_toColex_of_ssubset {α : Type u_1} [] {s : } {t : } (h : s t) :
{ ofColex := s } < { ofColex := t }

If s ⊂ t, then s < t in the colex order. Note the converse does not hold, as inclusion does not form a linear order.

instance Finset.Colex.instOrderBot {α : Type u_1} [] :
Equations
• Finset.Colex.instOrderBot =
@[simp]
theorem Finset.Colex.toColex_empty {α : Type u_1} [] :
{ ofColex := } =
@[simp]
theorem Finset.Colex.ofColex_bot {α : Type u_1} [] :
.ofColex =
theorem Finset.Colex.forall_le_mono {α : Type u_1} [] {s : } {t : } {a : α} (hst : { ofColex := s } { ofColex := t }) (ht : bt, b a) (b : α) :
b sb a

If s ≤ t in colex, and all elements in t are small, then all elements in s are small.

theorem Finset.Colex.forall_lt_mono {α : Type u_1} [] {s : } {t : } {a : α} (hst : { ofColex := s } { ofColex := t }) (ht : bt, b < a) (b : α) :
b sb < a

If s ≤ t in colex, and all elements in t are small, then all elements in s are small.

theorem Finset.Colex.toColex_le_singleton {α : Type u_1} [] {s : } {a : α} :
{ ofColex := s } { ofColex := {a} } bs, b a (a sb = a)

s ≤ {a} in colex iff all elements of s are strictly less than a, except possibly a in which case s = {a}.

theorem Finset.Colex.toColex_lt_singleton {α : Type u_1} [] {s : } {a : α} :
{ ofColex := s } < { ofColex := {a} } bs, b < a

s < {a} in colex iff all elements of s are strictly less than a.

theorem Finset.Colex.singleton_le_toColex {α : Type u_1} [] {s : } {a : α} :
{ ofColex := {a} } { ofColex := s } xs, a x

{a} ≤ s in colex iff s contains an element greated than or equal to a.

theorem Finset.Colex.singleton_le_singleton {α : Type u_1} [] {a : α} {b : α} :
{ ofColex := {a} } { ofColex := {b} } a b

Colex is an extension of the base order.

theorem Finset.Colex.singleton_lt_singleton {α : Type u_1} [] {a : α} {b : α} :
{ ofColex := {a} } < { ofColex := {b} } a < b

Colex is an extension of the base order.

instance Finset.Colex.instDecidableEq {α : Type u_1} [] :
Equations
instance Finset.Colex.instDecidableLE {α : Type u_1} [] [] [DecidableRel fun (x x_1 : α) => x x_1] :
DecidableRel fun (x x_1 : ) => x x_1
Equations
• s.instDecidableLE t = decidable_of_iff' (∀ ⦃a : α⦄, a s.ofColexat.ofColexbt.ofColex, bs.ofColex a b)
instance Finset.Colex.instDecidableLT {α : Type u_1} [] [] [DecidableRel fun (x x_1 : α) => x x_1] :
DecidableRel fun (x x_1 : ) => x < x_1
Equations
• Finset.Colex.instDecidableLT = decidableLTOfDecidableLE
theorem Finset.Colex.le_iff_sdiff_subset_lowerClosure {α : Type u_1} [] {s : } {t : } :
s t s.ofColex \ t.ofColex (lowerClosure (t.ofColex \ s.ofColex))
theorem Finset.Colex.toColex_sdiff_le_toColex_sdiff {α : Type u_1} [] {s : } {t : } {u : } [] (hus : u s) (hut : u t) :
{ ofColex := s \ u } { ofColex := t \ u } { ofColex := s } { ofColex := t }

The colexigraphic order is insensitive to removing the same elements from both sets.

theorem Finset.Colex.toColex_sdiff_lt_toColex_sdiff {α : Type u_1} [] {s : } {t : } {u : } [] (hus : u s) (hut : u t) :
{ ofColex := s \ u } < { ofColex := t \ u } { ofColex := s } < { ofColex := t }

The colexigraphic order is insensitive to removing the same elements from both sets.

@[simp]
theorem Finset.Colex.toColex_sdiff_le_toColex_sdiff' {α : Type u_1} [] {s : } {t : } [] :
{ ofColex := s \ t } { ofColex := t \ s } { ofColex := s } { ofColex := t }
@[simp]
theorem Finset.Colex.toColex_sdiff_lt_toColex_sdiff' {α : Type u_1} [] {s : } {t : } [] :
{ ofColex := s \ t } < { ofColex := t \ s } { ofColex := s } < { ofColex := t }
instance Finset.Colex.instLinearOrder {α : Type u_1} [] :
Equations
• Finset.Colex.instLinearOrder = LinearOrder.mk Finset.Colex.instDecidableLE decidableEqOfDecidableLE Finset.Colex.instDecidableLT
theorem Finset.Colex.toColex_lt_toColex_iff_exists_forall_lt {α : Type u_1} [] {s : } {t : } :
{ ofColex := s } < { ofColex := t } at, as bs, btb < a
theorem Finset.Colex.lt_iff_exists_forall_lt {α : Type u_1} [] {s : } {t : } :
s < t at.ofColex, as.ofColex bs.ofColex, bt.ofColexb < a
theorem Finset.Colex.toColex_le_toColex_iff_max'_mem {α : Type u_1} [] {s : } {t : } :
{ ofColex := s } { ofColex := t } ∀ (hst : s t), (symmDiff s t).max' t
theorem Finset.Colex.le_iff_max'_mem {α : Type u_1} [] {s : } {t : } :
s t ∀ (h : s t), (symmDiff s.ofColex t.ofColex).max' t.ofColex
theorem Finset.Colex.toColex_lt_toColex_iff_max'_mem {α : Type u_1} [] {s : } {t : } :
{ ofColex := s } < { ofColex := t } ∃ (hst : s t), (symmDiff s t).max' t
theorem Finset.Colex.lt_iff_max'_mem {α : Type u_1} [] {s : } {t : } :
s < t ∃ (h : s t), (symmDiff s.ofColex t.ofColex).max' t.ofColex
theorem Finset.Colex.toColex_image_le_toColex_image {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : } {t : } (hf : ) :
{ ofColex := } { ofColex := } { ofColex := s } { ofColex := t }

Strictly monotone functions preserve the colex ordering.

theorem Finset.Colex.toColex_image_lt_toColex_image {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : } {t : } (hf : ) :
{ ofColex := } < { ofColex := } { ofColex := s } < { ofColex := t }

Strictly monotone functions preserve the colex ordering.

theorem Finset.Colex.toColex_image_ofColex_strictMono {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
StrictMono fun (s : ) => { ofColex := Finset.image f s.ofColex }

Initial segments #

def Finset.Colex.IsInitSeg {α : Type u_1} [] (𝒜 : Finset ()) (r : ) :

𝒜 is an initial segment of the colexigraphic order on sets of r, and that if t is below s in colex where t has size r and s is in 𝒜, then t is also in 𝒜. In effect, 𝒜 is downwards closed with respect to colex among sets of size r.

Equations
• = (Set.Sized r 𝒜 ∀ ⦃s t : ⦄, s 𝒜{ ofColex := t } < { ofColex := s } t.card = rt 𝒜)
Instances For
@[simp]
theorem Finset.Colex.isInitSeg_empty {α : Type u_1} [] {r : } :
theorem Finset.Colex.IsInitSeg.total {α : Type u_1} [] {𝒜₁ : Finset ()} {𝒜₂ : Finset ()} {r : } (h₁ : ) (h₂ : ) :
𝒜₁ 𝒜₂ 𝒜₂ 𝒜₁

Initial segments are nested in some way. In particular, if they're the same size they're equal.

def Finset.Colex.initSeg {α : Type u_1} [] [] (s : ) :

The initial segment of the colexicographic order on sets with s.card elements and ending at s.

Equations
Instances For
@[simp]
theorem Finset.Colex.mem_initSeg {α : Type u_1} [] {s : } {t : } [] :
s.card = t.card { ofColex := t } { ofColex := s }
theorem Finset.Colex.mem_initSeg_self {α : Type u_1} [] {s : } [] :
@[simp]
theorem Finset.Colex.initSeg_nonempty {α : Type u_1} [] {s : } [] :
.Nonempty
theorem Finset.Colex.isInitSeg_initSeg {α : Type u_1} [] {s : } [] :
theorem Finset.Colex.IsInitSeg.exists_initSeg {α : Type u_1} [] {𝒜 : Finset ()} {r : } [] (h𝒜 : ) (h𝒜₀ : 𝒜.Nonempty) :
∃ (s : ), s.card = r
theorem Finset.Colex.isInitSeg_iff_exists_initSeg {α : Type u_1} [] {𝒜 : Finset ()} {r : } [] :
𝒜.Nonempty ∃ (s : ), s.card = r

Being a nonempty initial segment of colex is equivalent to being an initSeg.

Colex on ℕ#

The colexicographic order agrees with the order induced by interpreting a set of naturals as a n-ary expansion.

theorem Finset.geomSum_ofColex_strictMono {n : } (hn : 2 n) :
StrictMono fun (s : ) => ks.ofColex, n ^ k
theorem Finset.geomSum_le_geomSum_iff_toColex_le_toColex {s : } {t : } {n : } (hn : 2 n) :
ks, n ^ k kt, n ^ k { ofColex := s } { ofColex := t }

For finsets of naturals of naturals, the colexicographic order is equivalent to the order induced by the n-ary expansion.

theorem Finset.geomSum_lt_geomSum_iff_toColex_lt_toColex {s : } {t : } {n : } (hn : 2 n) :
is, n ^ i < it, n ^ i { ofColex := s } < { ofColex := t }

For finsets of naturals of naturals, the colexicographic order is equivalent to the order induced by the n-ary expansion.