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.

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

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

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

• )

theorem Finset.Colex.ext_iff {α : Type u_3} {x y : Colex α} : x = y ↔ x.ofColex = y.ofColex

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

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

Equations

• Finset.instInhabitedColex = { default := { ofColex := ∅ } }

@[simp]

theorem Finset.toColex_ofColex {α : Type u_1} (s : Colex α) : { ofColex := s.ofColex } = s

theorem Finset.ofColex_toColex {α : Type u_1} (s : Finset α) : { ofColex := s }.ofColex = s

theorem Finset.toColex_inj {α : Type u_1} {s t : Finset α} : { ofColex := s } = { ofColex := t } ↔ s = t

@[simp]

theorem Finset.ofColex_inj {α : Type u_1} {s t : Colex α} : s.ofColex = t.ofColex ↔ s = t

theorem Finset.toColex_ne_toColex {α : Type u_1} {s t : Finset α} : { ofColex := s } ≠ { ofColex := t } ↔ s ≠ t

theorem Finset.ofColex_ne_ofColex {α : Type u_1} {s t : Colex α} : s.ofColex ≠ t.ofColex ↔ s ≠ t

theorem Finset.toColex_injective {α : Type u_1} : Function.Injective Colex.toColex

theorem Finset.ofColex_injective {α : Type u_1} : Function.Injective Colex.ofColex

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

Equations

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

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

Equations

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

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

theorem Finset.Colex.toColex_le_toColex {α : Type u_1} [PartialOrder α] {s t : Finset α} : { ofColex := s } ≤ { ofColex := 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 α} : { ofColex := s } < { ofColex := 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) : { 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} [PartialOrder α] {s t : Finset α} (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} [PartialOrder α] : OrderBot (Colex α)

Equations

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

@[simp]

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

@[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 : { ofColex := s } ≤ { ofColex := 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 : { ofColex := s } ≤ { ofColex := 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 : α} : { ofColex := s } ≤ { ofColex := {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 : α} : { ofColex := s } < { ofColex := {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 : α} : { ofColex := {a} } ≤ { ofColex := 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 : α} : { ofColex := {a} } ≤ { ofColex := {b} } ↔ a ≤ b

Colex is an extension of the base order.

theorem Finset.Colex.singleton_lt_singleton {α : Type u_1} [PartialOrder α] {a b : α} : { ofColex := {a} } < { ofColex := {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 α} : s ≤ t ↔ ↑s.ofColex \ ↑t.ofColex ⊆ ↑(lowerClosure (↑t.ofColex \ ↑s.ofColex))

instance Finset.Colex.instDecidableEq {α : Type u_1} [DecidableEq α] : DecidableEq (Colex α)

Equations

• s.instDecidableEq t = decidable_of_iff' (s.ofColex = t.ofColex) ⋯

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

Equations

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

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

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) : { 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} [PartialOrder α] {s t u : Finset α} [DecidableEq α] (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} [PartialOrder α] {s t : Finset α} [DecidableEq α] : { ofColex := s \ t } ≤ { ofColex := t \ s } ↔ { ofColex := s } ≤ { ofColex := t }

@[simp]

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

@[simp]

theorem Finset.Colex.cons_le_cons {α : Type u_1} [PartialOrder α] {s : Finset α} {a b : α} (ha : a ∉ s) (hb : b ∉ s) : { ofColex := cons a s ha } ≤ { ofColex := 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) : { ofColex := cons a s ha } < { ofColex := 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) : { ofColex := insert a s } ≤ { ofColex := 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) : { ofColex := insert a s } < { ofColex := 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) : { ofColex := s.erase a } ≤ { ofColex := 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) : { ofColex := s.erase a } < { ofColex := s.erase b } ↔ b < a

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

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 α} : { ofColex := s } < { ofColex := 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 α} : s < t ↔ ∃ a ∈ t.ofColex, a ∉ s.ofColex ∧ ∀ b ∈ s.ofColex, b ∉ t.ofColex → b < a

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

theorem Finset.Colex.le_iff_max'_mem {α : Type u_1} [LinearOrder α] {s t : Colex α} : 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} [LinearOrder α] {s t : Finset α} : { ofColex := s } < { ofColex := t } ↔ ∃ (hst : s ≠ t), (symmDiff s t).max' ⋯ ∈ t

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

theorem Finset.Colex.lt_iff_exists_filter_lt {α : Type u_1} [LinearOrder α] {s t : Finset α} : { ofColex := s } < { ofColex := 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 : { ofColex := s } ≤ { ofColex := t }) (hcard : s.card ≤ t.card) (ha : a ∈ s) : { ofColex := s.erase a } ≤ { ofColex := 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) : { ofColex := image f s } ≤ { ofColex := image f t } ↔ { 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} [LinearOrder α] [LinearOrder β] {f : α → β} {s t : Finset α} (hf : StrictMono f) : { ofColex := image f s } < { ofColex := image f t } ↔ { ofColex := s } < { ofColex := 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 α) => { ofColex := image f s.ofColex }

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

Equations

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

@[simp]

theorem Finset.Colex.toColex_univ {α : Type u_1} [LinearOrder α] [Fintype α] : { ofColex := 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 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

• Finset.Colex.IsInitSeg 𝒜 r = (Set.Sized r ↑𝒜 ∧ ∀ ⦃s t : Finset α⦄, s ∈ 𝒜 → { ofColex := t } < { ofColex := 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 ∧ { ofColex := t } ≤ { ofColex := s }}

@[simp]

theorem Finset.Colex.mem_initSeg {α : Type u_1} [LinearOrder α] {s t : Finset α} [Fintype α] : t ∈ initSeg s ↔ s.card = t.card ∧ { ofColex := t } ≤ { ofColex := 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 ℕ) => ∑ k ∈ s.ofColex, 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 ↔ { ofColex := s } ≤ { ofColex := 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 ↔ { ofColex := s } < { ofColex := 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_twoPowSum (s : Finset ℕ) : (∑ i ∈ s, 2 ^ i).bitIndices.toFinset = s

@[simp]

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

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_symm_apply (s : Finset ℕ) : equivBitIndices.symm s = ∑ i ∈ s, 2 ^ i

@[simp]

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

def Finset.orderIsoColex : ℕ ≃o Colex ℕ

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 ℕ) : (RelIso.symm orderIsoColex) s = equivBitIndices.symm s.ofColex

@[simp]

theorem Finset.orderIsoColex_apply_ofColex (n : ℕ) : (orderIsoColex n).ofColex = equivBitIndices n