Documentation

Mathlib.Combinatorics.Colex

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

)

Instances For

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

@[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 α] :

Equations

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

PartialOrder (Colex α)

Equations

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

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

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

DecidableLE (Colex α)

Equations

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

DecidableLT (Colex α)

Equations

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

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

@[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 : ℕ) :

𝒜 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

Instances For

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

Instances For

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

Instances For

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

Instances For

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