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 #

See also #

Related files are:

TODO #

References #

Tags #

colex, colexicographic, binary

@[deprecated Colex (since := "2025-08-28")]
structure Finset.Colex (α : Type u_3) :
Type u_3

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

Instances For
    @[deprecated toColex_ofColex (since := "2025-08-28")]
    theorem Finset.toColex_ofColex {α : Type u_1} (s : Finset.Colex α) :
    { ofColex := s.ofColex } = s
    @[deprecated ofColex_toColex (since := "2025-08-28")]
    theorem Finset.ofColex_toColex {α : Type u_1} (s : Finset α) :
    { ofColex := s }.ofColex = s
    @[deprecated toColex_inj (since := "2025-08-28")]
    theorem Finset.toColex_inj {α : Type u_1} {s t : Finset α} :
    { ofColex := s } = { ofColex := t } s = t
    @[deprecated ofColex_inj (since := "2025-08-28")]
    theorem Finset.ofColex_inj {α : Type u_1} {s t : Finset.Colex α} :
    @[deprecated toColex_inj (since := "2025-08-28")]
    theorem Finset.toColex_ne_toColex {α : Type u_1} {s t : Finset α} :
    { ofColex := s } { ofColex := t } s t
    @[deprecated ofColex_inj (since := "2025-08-28")]
    theorem Finset.ofColex_ne_ofColex {α : Type u_1} {s t : Finset.Colex α} :
    @[deprecated toColex_inj (since := "2025-08-28")]
    @[deprecated ofColex_inj (since := "2025-08-28")]
    instance Finset.Colex.instLE {α : Type u_1} [PartialOrder α] :
    LE (Colex (Finset α))
    Equations
    Equations
    theorem Finset.Colex.le_def {α : Type u_1} [PartialOrder α] {s t : Colex (Finset α)} :
    s t ∀ ⦃a : α⦄, a ofColex saofColex tbofColex t, bofColex s a b
    theorem Finset.Colex.toColex_le_toColex {α : Type u_1} [PartialOrder α] {s t : Finset α} :
    toColex s toColex t ∀ ⦃a : α⦄, a satbt, bs a b
    theorem Finset.Colex.toColex_lt_toColex {α : Type u_1} [PartialOrder α] {s t : Finset α} :
    toColex s < toColex t s t ∀ ⦃a : α⦄, a satbt, bs a b

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

    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) :

    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) :

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

    Equations
    theorem Finset.Colex.forall_le_mono {α : Type u_1} [PartialOrder α] {s t : Finset α} {a : α} (hst : toColex s toColex 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} [PartialOrder α] {s t : Finset α} {a : α} (hst : toColex s toColex 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} [PartialOrder α] {s : Finset α} {a : α} :
    toColex s toColex {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} [PartialOrder α] {s : Finset α} {a : α} :
    toColex s < toColex {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} [PartialOrder α] {s : Finset α} {a : α} :
    toColex {a} toColex s xs, a x

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

    Colex is an extension of the base order.

    theorem Finset.Colex.singleton_lt_singleton {α : Type u_1} [PartialOrder α] {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)))
    Equations
    theorem Finset.Colex.toColex_sdiff_le_toColex_sdiff {α : Type u_1} [PartialOrder α] {s t u : Finset α} [DecidableEq α] (hus : u s) (hut : u 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) :
    toColex (s \ u) < toColex (t \ u) toColex s < toColex t

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

    @[simp]
    theorem Finset.Colex.cons_le_cons {α : Type u_1} [PartialOrder α] {s : Finset α} {a b : α} (ha : as) (hb : bs) :
    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 : as) (hb : bs) :
    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 : as) (hb : bs) :
    theorem Finset.Colex.insert_lt_insert {α : Type u_1} [PartialOrder α] {s : Finset α} {a b : α} [DecidableEq α] (ha : as) (hb : bs) :
    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
    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 at, as bs, btb < a
    theorem Finset.Colex.lt_iff_exists_forall_lt {α : Type u_1} [LinearOrder α] {s t : Colex (Finset α)} :
    s < t aofColex t, aofColex s bofColex s, bofColex tb < 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 wt \ s, {as | w < a} = {at | 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) :

    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) :

    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))
    @[simp]

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

      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 α] :
        theorem Finset.Colex.mem_initSeg_self {α : Type u_1} [LinearOrder α] {s : Finset α} [Fintype α] :
        @[simp]
        theorem Finset.Colex.initSeg_nonempty {α : Type u_1} [LinearOrder α] {s : Finset α} [Fintype α] :
        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 )) => kofColex s, n ^ k
        theorem Finset.geomSum_le_geomSum_iff_toColex_le_toColex {s t : Finset } {n : } (hn : 2 n) :
        ks, n ^ k kt, 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) :
        is, n ^ i < it, 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 ) => is, n ^ i
        theorem Finset.lt_geomSum_of_mem {s : Finset } {n a : } (hn : 2 n) (hi : a s) :
        a < is, n ^ i
        @[simp]
        @[simp]

        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.
        Instances For
          @[simp]

          The equivalence Nat.equivBitIndices enumerates Finset in colexicographic order.

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