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

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

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

@[implicit_reducible]

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

Equations

• Finset.Colex.instLE = { le := fun (s t : Colex (Finset α)) => ∀ ⦃a : α⦄, a ∈ ofColex s → a ∉ ofColex t → ∃ b ∈ ofColex t, b ∉ ofColex s ∧ a ≤ b }

@[implicit_reducible]

instance Finset.Colex.instPartialOrder {α : Type u_1} [PartialOrder α] : PartialOrder (Colex (Finset α))

Equations

• Finset.Colex.instPartialOrder = { toLE := Finset.Colex.instLE, lt := fun (a b : Colex (Finset α)) => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

theorem Finset.Colex.le_def {α : Type u_1} [PartialOrder α] {s t : Colex (Finset α)} : s ≤ t ↔ ∀ ⦃a : α⦄, a ∈ ofColex s → a ∉ ofColex t → ∃ b ∈ ofColex t, b ∉ ofColex s ∧ a ≤ b

theorem Finset.Colex.toColex_le_toColex {α : Type u_1} [PartialOrder α] {s t : Finset α} : toColex s ≤ toColex t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b

theorem Finset.Colex.toColex_lt_toColex {α : Type u_1} [PartialOrder α] {s t : Finset α} : toColex s < toColex t ↔ s ≠ t ∧ ∀ ⦃a : α⦄, a ∈ s → a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b

theorem Finset.Colex.toColex_mono {α : Type u_1} [PartialOrder α] : Monotone ⇑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} [PartialOrder α] : StrictMono ⇑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} [PartialOrder α] {s t : Finset α} (h : s ⊆ t) : toColex s ≤ toColex 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} [PartialOrder α] {s t : Finset α} (h : s ⊂ t) : toColex s < toColex 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.

@[implicit_reducible]

instance Finset.Colex.instOrderBot {α : Type u_1} [PartialOrder α] : OrderBot (Colex (Finset α))

Equations

• Finset.Colex.instOrderBot = { bot := toColex ∅, bot_le := ⋯ }

@[simp]

theorem Finset.Colex.toColex_empty {α : Type u_1} [PartialOrder α] : toColex ∅ = ⊥

@[simp]

theorem Finset.Colex.ofColex_bot {α : Type u_1} [PartialOrder α] : ofColex ⊥ = ∅

theorem Finset.Colex.forall_le_mono {α : Type u_1} [PartialOrder α] {s t : Finset α} {a : α} (hst : toColex s ≤ toColex t) (ht : ∀ b ∈ t, b ≤ a) (b : α) : b ∈ s → b ≤ 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} [PartialOrder α] {s t : Finset α} {a : α} (hst : toColex s ≤ toColex t) (ht : ∀ b ∈ t, b < a) (b : α) : b ∈ s → b < 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} [PartialOrder α] {s : Finset α} {a : α} : toColex s ≤ toColex {a} ↔ ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = 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} [PartialOrder α] {s : Finset α} {a : α} : toColex s < toColex {a} ↔ ∀ b ∈ s, 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} [PartialOrder α] {s : Finset α} {a : α} : toColex {a} ≤ toColex s ↔ ∃ x ∈ s, a ≤ x

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

theorem Finset.Colex.singleton_le_singleton {α : Type u_1} [PartialOrder α] {a b : α} : toColex {a} ≤ toColex {b} ↔ a ≤ b

Colex is an extension of the base order.

theorem Finset.Colex.singleton_lt_singleton {α : Type u_1} [PartialOrder α] {a b : α} : toColex {a} < toColex {b} ↔ a < b

Colex is an extension of the base order.

theorem Finset.Colex.le_iff_sdiff_subset_lowerClosure {α : Type u_1} [PartialOrder α] {s t : Colex (Finset α)} : s ≤ t ↔ ↑(ofColex s) \ ↑(ofColex t) ⊆ ↑(lowerClosure (↑(ofColex t) \ ↑(ofColex s)))

@[implicit_reducible]

instance Finset.Colex.instDecidableLE {α : Type u_1} [PartialOrder α] [DecidableEq α] [DecidableLE α] : DecidableLE (Colex (Finset α))

Equations

• Finset.Colex.instDecidableLE s t = decidable_of_iff' (∀ ⦃a : α⦄, a ∈ ofColex s → a ∉ ofColex t → ∃ b ∈ ofColex t, b ∉ ofColex s ∧ a ≤ b) ⋯

@[implicit_reducible]

instance Finset.Colex.instDecidableLT {α : Type u_1} [PartialOrder α] [DecidableEq α] [DecidableLE α] : DecidableLT (Colex (Finset α))

Equations

• Finset.Colex.instDecidableLT = decidableLTOfDecidableLE

theorem Finset.Colex.toColex_sdiff_le_toColex_sdiff {α : Type u_1} [PartialOrder α] {s t u : Finset α} [DecidableEq α] (hus : u ⊆ s) (hut : u ⊆ t) : toColex (s \ u) ≤ toColex (t \ u) ↔ toColex s ≤ toColex t

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

theorem Finset.Colex.toColex_sdiff_lt_toColex_sdiff {α : Type u_1} [PartialOrder α] {s t u : Finset α} [DecidableEq α] (hus : u ⊆ s) (hut : u ⊆ t) : toColex (s \ u) < toColex (t \ u) ↔ toColex s < toColex t

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

@[simp]

theorem Finset.Colex.toColex_sdiff_le_toColex_sdiff' {α : Type u_1} [PartialOrder α] {s t : Finset α} [DecidableEq α] : toColex (s \ t) ≤ toColex (t \ s) ↔ toColex s ≤ toColex t

@[simp]

theorem Finset.Colex.toColex_sdiff_lt_toColex_sdiff' {α : Type u_1} [PartialOrder α] {s t : Finset α} [DecidableEq α] : toColex (s \ t) < toColex (t \ s) ↔ toColex s < toColex t

@[simp]

theorem Finset.Colex.cons_le_cons {α : Type u_1} [PartialOrder α] {s : Finset α} {a b : α} (ha : a ∉ s) (hb : b ∉ s) : toColex (cons a s ha) ≤ toColex (cons b s hb) ↔ a ≤ b

@[simp]

theorem Finset.Colex.cons_lt_cons {α : Type u_1} [PartialOrder α] {s : Finset α} {a b : α} (ha : a ∉ s) (hb : b ∉ s) : toColex (cons a s ha) < toColex (cons b s hb) ↔ a < b

theorem Finset.Colex.insert_le_insert {α : Type u_1} [PartialOrder α] {s : Finset α} {a b : α} [DecidableEq α] (ha : a ∉ s) (hb : b ∉ s) : toColex (insert a s) ≤ toColex (insert b s) ↔ a ≤ b

theorem Finset.Colex.insert_lt_insert {α : Type u_1} [PartialOrder α] {s : Finset α} {a b : α} [DecidableEq α] (ha : a ∉ s) (hb : b ∉ s) : toColex (insert a s) < toColex (insert b s) ↔ a < b

theorem Finset.Colex.erase_le_erase {α : Type u_1} [PartialOrder α] {s : Finset α} {a b : α} [DecidableEq α] (ha : a ∈ s) (hb : b ∈ s) : toColex (s.erase a) ≤ toColex (s.erase b) ↔ b ≤ a

theorem Finset.Colex.erase_lt_erase {α : Type u_1} [PartialOrder α] {s : Finset α} {a b : α} [DecidableEq α] (ha : a ∈ s) (hb : b ∈ s) : toColex (s.erase a) < toColex (s.erase b) ↔ b < a

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

theorem Finset.Colex.toColex_lt_toColex_iff_exists_forall_lt {α : Type u_1} [LinearOrder α] {s t : Finset α} : toColex s < toColex t ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a

theorem Finset.Colex.lt_iff_exists_forall_lt {α : Type u_1} [LinearOrder α] {s t : Colex (Finset α)} : s < t ↔ ∃ a ∈ ofColex t, a ∉ ofColex s ∧ ∀ b ∈ ofColex s, b ∉ ofColex t → b < a

theorem Finset.Colex.toColex_le_toColex_iff_max'_mem {α : Type u_1} [LinearOrder α] {s t : Finset α} : toColex s ≤ toColex t ↔ ∀ (hst : s ≠ t), (symmDiff s t).max' ⋯ ∈ t

theorem Finset.Colex.le_iff_max'_mem {α : Type u_1} [LinearOrder α] {s t : Colex (Finset α)} : s ≤ t ↔ ∀ (h : s ≠ t), (symmDiff (ofColex s) (ofColex t)).max' ⋯ ∈ ofColex t

theorem Finset.Colex.toColex_lt_toColex_iff_max'_mem {α : Type u_1} [LinearOrder α] {s t : Finset α} : toColex s < toColex t ↔ ∃ (hst : s ≠ t), (symmDiff s t).max' ⋯ ∈ t

theorem Finset.Colex.lt_iff_max'_mem {α : Type u_1} [LinearOrder α] {s t : Colex (Finset α)} : s < t ↔ ∃ (h : s ≠ t), (symmDiff (ofColex s) (ofColex t)).max' ⋯ ∈ ofColex t

theorem Finset.Colex.lt_iff_exists_filter_lt {α : Type u_1} [LinearOrder α] {s t : Finset α} : toColex s < toColex t ↔ ∃ w ∈ t \ s, {a ∈ s | w < a} = {a ∈ t | w < a}

theorem Finset.Colex.erase_le_erase_min' {α : Type u_1} [LinearOrder α] {s t : Finset α} {a : α} (hst : toColex s ≤ toColex t) (hcard : s.card ≤ t.card) (ha : a ∈ s) : toColex (s.erase a) ≤ toColex (t.erase (t.min' ⋯))

If s ≤ t in colex and #s ≤ #t, then s \ {a} ≤ t \ {min t} for any a ∈ s.

theorem Finset.Colex.toColex_image_le_toColex_image {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} {s t : Finset α} (hf : StrictMono f) : toColex (image f s) ≤ toColex (image f t) ↔ toColex s ≤ toColex t

Strictly monotone functions preserve the colex ordering.

theorem Finset.Colex.toColex_image_lt_toColex_image {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} {s t : Finset α} (hf : StrictMono f) : toColex (image f s) < toColex (image f t) ↔ toColex s < toColex t

Strictly monotone functions preserve the colex ordering.

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

@[implicit_reducible]

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

Equations

• Finset.Colex.instBoundedOrder = { top := toColex Finset.univ, le_top := ⋯, toOrderBot := Finset.Colex.instOrderBot }

@[simp]

theorem Finset.Colex.toColex_univ {α : Type u_1} [LinearOrder α] [Fintype α] : toColex univ = ⊤

@[simp]

theorem Finset.Colex.ofColex_top {α : Type u_1} [LinearOrder α] [Fintype α] : ofColex ⊤ = univ

Initial segments

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

𝒜 is an initial segment of the colexicographic 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

• Finset.Colex.IsInitSeg 𝒜 r = (Set.Sized r ↑𝒜 ∧ ∀ ⦃s t : Finset α⦄, s ∈ 𝒜 → toColex t < toColex s ∧ t.card = r → t ∈ 𝒜)

@[simp]

theorem Finset.Colex.isInitSeg_empty {α : Type u_1} [LinearOrder α] {r : ℕ} : IsInitSeg ∅ r

theorem Finset.Colex.IsInitSeg.total {α : Type u_1} [LinearOrder α] {𝒜₁ 𝒜₂ : Finset (Finset α)} {r : ℕ} (h₁ : IsInitSeg 𝒜₁ r) (h₂ : IsInitSeg 𝒜₂ r) : 𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁

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} [LinearOrder α] [Fintype α] (s : Finset α) : Finset (Finset α)

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

Equations

• Finset.Colex.initSeg s = {t : Finset α | s.card = t.card ∧ toColex t ≤ toColex s}

@[simp]

theorem Finset.Colex.mem_initSeg {α : Type u_1} [LinearOrder α] {s t : Finset α} [Fintype α] : t ∈ initSeg s ↔ s.card = t.card ∧ toColex t ≤ toColex s

theorem Finset.Colex.mem_initSeg_self {α : Type u_1} [LinearOrder α] {s : Finset α} [Fintype α] : s ∈ initSeg s

@[simp]

theorem Finset.Colex.initSeg_nonempty {α : Type u_1} [LinearOrder α] {s : Finset α} [Fintype α] : (initSeg s).Nonempty

theorem Finset.Colex.isInitSeg_initSeg {α : Type u_1} [LinearOrder α] {s : Finset α} [Fintype α] : IsInitSeg (initSeg s) s.card

theorem Finset.Colex.IsInitSeg.exists_initSeg {α : Type u_1} [LinearOrder α] {𝒜 : Finset (Finset α)} {r : ℕ} [Fintype α] (h𝒜 : IsInitSeg 𝒜 r) (h𝒜₀ : 𝒜.Nonempty) : ∃ (s : Finset α), s.card = r ∧ 𝒜 = initSeg s

theorem Finset.Colex.isInitSeg_iff_exists_initSeg {α : Type u_1} [LinearOrder α] {𝒜 : Finset (Finset α)} {r : ℕ} [Fintype α] : IsInitSeg 𝒜 r ∧ 𝒜.Nonempty ↔ ∃ (s : Finset α), s.card = r ∧ 𝒜 = initSeg s

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 : Colex (Finset ℕ)) => ∑ k ∈ ofColex s, n ^ k

theorem Finset.geomSum_le_geomSum_iff_toColex_le_toColex {s t : Finset ℕ} {n : ℕ} (hn : 2 ≤ n) : ∑ k ∈ s, n ^ k ≤ ∑ k ∈ t, n ^ k ↔ toColex s ≤ toColex t

For finsets 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 : Finset ℕ} {n : ℕ} (hn : 2 ≤ n) : ∑ i ∈ s, n ^ i < ∑ i ∈ t, n ^ i ↔ toColex s < toColex t

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

theorem Finset.geomSum_injective {n : ℕ} (hn : 2 ≤ n) : Function.Injective fun (s : Finset ℕ) => ∑ i ∈ s, n ^ i

theorem Finset.lt_geomSum_of_mem {s : Finset ℕ} {n a : ℕ} (hn : 2 ≤ n) (hi : a ∈ s) : a < ∑ i ∈ s, n ^ i

@[simp]

theorem Finset.toFinset_bitIndices_sum_two_pow (s : Finset ℕ) : (∑ i ∈ s, 2 ^ i).bitIndices.toFinset = s

@[simp]

theorem Finset.sum_toFinset_bitIndices_two_pow (n : ℕ) : ∑ i ∈ n.bitIndices.toFinset, 2 ^ i = n

@[deprecated Finset.toFinset_bitIndices_sum_two_pow (since := "2026-05-15")]

theorem Finset.toFinset_bitIndices_twoPowSum (s : Finset ℕ) : (∑ i ∈ s, 2 ^ i).bitIndices.toFinset = s

Alias of Finset.toFinset_bitIndices_sum_two_pow.

@[deprecated Finset.sum_toFinset_bitIndices_two_pow (since := "2026-05-15")]

theorem Finset.twoPowSum_toFinset_bitIndices (n : ℕ) : ∑ i ∈ n.bitIndices.toFinset, 2 ^ i = n

Alias of Finset.sum_toFinset_bitIndices_two_pow.

def Finset.equivBitIndices : ℕ ≃ Finset ℕ

The equivalence between ℕ and Finset ℕ that maps ∑ i ∈ s, 2^i to s.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Finset.equivBitIndices_apply (n : ℕ) : equivBitIndices n = n.bitIndices.toFinset

@[simp]

theorem Finset.equivBitIndices_symm_apply (s : Finset ℕ) : equivBitIndices.symm s = ∑ i ∈ s, 2 ^ i

def Finset.orderIsoColex : ℕ ≃o Colex (Finset ℕ)

The equivalence Nat.equivBitIndices enumerates Finset ℕ in colexicographic order.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Finset.orderIsoColex_symm_apply (s : Colex (Finset ℕ)) : (RelIso.symm orderIsoColex) s = equivBitIndices.symm (ofColex s)

@[simp]

theorem Finset.orderIsoColex_apply (n : ℕ) : orderIsoColex n = toColex (equivBitIndices n)