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

theorem Finset.Colex.ext {α : Type u_3} {x : Finset.Colex α} {y : Finset.Colex α} (ofColex : x.ofColex = y.ofColex) :
x = y
theorem Finset.Colex.ext_iff {α : Type u_3} {x : Finset.Colex α} {y : Finset.Colex α} :
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.

Instances For
    Equations
    • Finset.instInhabitedColex = { default := { ofColex := } }
    @[simp]
    theorem Finset.toColex_ofColex {α : Type u_1} (s : Finset.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 : Finset α} {t : Finset α} :
    { ofColex := s } = { ofColex := t } s = t
    @[simp]
    theorem Finset.ofColex_inj {α : Type u_1} {s : Finset.Colex α} {t : Finset.Colex α} :
    s.ofColex = t.ofColex s = t
    theorem Finset.toColex_ne_toColex {α : Type u_1} {s : Finset α} {t : Finset α} :
    { ofColex := s } { ofColex := t } s t
    theorem Finset.ofColex_ne_ofColex {α : Type u_1} {s : Finset.Colex α} {t : Finset.Colex α} :
    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} [PartialOrder α] :
    Equations
    • Finset.Colex.instLE = { le := fun (s t : Finset.Colex α) => ∀ ⦃a : α⦄, a s.ofColexat.ofColexbt.ofColex, bs.ofColex a b }
    Equations
    theorem Finset.Colex.le_def {α : Type u_1} [PartialOrder α] {s : Finset.Colex α} {t : Finset.Colex α} :
    s t ∀ ⦃a : α⦄, a s.ofColexat.ofColexbt.ofColex, bs.ofColex a b
    theorem Finset.Colex.toColex_le_toColex {α : Type u_1} [PartialOrder α] {s : Finset α} {t : Finset α} :
    { ofColex := s } { ofColex := t } ∀ ⦃a : α⦄, a satbt, bs a b
    theorem Finset.Colex.toColex_lt_toColex {α : Type u_1} [PartialOrder α] {s : Finset α} {t : Finset α} :
    { ofColex := s } < { ofColex := t } s t ∀ ⦃a : α⦄, a satbt, bs a b
    theorem Finset.Colex.toColex_mono {α : Type u_1} [PartialOrder α] :
    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} [PartialOrder α] :
    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} [PartialOrder α] {s : Finset α} {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 : Finset α} {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.

    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 : Finset α} {t : Finset α} {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} [PartialOrder α] {s : Finset α} {t : Finset α} {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} [PartialOrder α] {s : Finset α} {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} [PartialOrder α] {s : Finset α} {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} [PartialOrder α] {s : Finset α} {a : α} :
    { ofColex := {a} } { ofColex := s } xs, 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 : Finset.Colex α} {t : Finset.Colex α} :
    s t s.ofColex \ t.ofColex (lowerClosure (t.ofColex \ s.ofColex))
    Equations
    instance Finset.Colex.instDecidableLE {α : Type u_1} [PartialOrder α] [DecidableEq α] [DecidableRel fun (x1 x2 : α) => x1 x2] :
    DecidableRel fun (x1 x2 : Finset.Colex α) => x1 x2
    Equations
    • s.instDecidableLE t = decidable_of_iff' (∀ ⦃a : α⦄, a s.ofColexat.ofColexbt.ofColex, bs.ofColex a b)
    instance Finset.Colex.instDecidableLT {α : Type u_1} [PartialOrder α] [DecidableEq α] [DecidableRel fun (x1 x2 : α) => x1 x2] :
    DecidableRel fun (x1 x2 : Finset.Colex α) => x1 < x2
    Equations
    • Finset.Colex.instDecidableLT = decidableLTOfDecidableLE
    theorem Finset.Colex.toColex_sdiff_le_toColex_sdiff {α : Type u_1} [PartialOrder α] {s : Finset α} {t : Finset α} {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 : Finset α} {t : Finset α} {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 : Finset α} {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 : Finset α} {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 : as) (hb : bs) :
    { ofColex := Finset.cons a s ha } { ofColex := Finset.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) :
    { ofColex := Finset.cons a s ha } < { ofColex := Finset.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) :
    { 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 : as) (hb : bs) :
    { 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
    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} [LinearOrder α] {s : Finset α} {t : Finset α} :
    { ofColex := s } < { ofColex := t } at, as bs, btb < a
    theorem Finset.Colex.lt_iff_exists_forall_lt {α : Type u_1} [LinearOrder α] {s : Finset.Colex α} {t : Finset.Colex α} :
    s < t at.ofColex, as.ofColex bs.ofColex, bt.ofColexb < a
    theorem Finset.Colex.toColex_le_toColex_iff_max'_mem {α : Type u_1} [LinearOrder α] {s : Finset α} {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 : Finset.Colex α} {t : Finset.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 : Finset α} {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 : Finset.Colex α} {t : Finset.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 : Finset α} {t : Finset α} :
    { ofColex := s } < { ofColex := t } wt \ s, Finset.filter (fun (x : α) => w < x) s = Finset.filter (fun (x : α) => w < x) t
    theorem Finset.Colex.erase_le_erase_min' {α : Type u_1} [LinearOrder α] {s : Finset α} {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.card ≤ t.card, 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 : Finset α} {t : Finset α} (hf : StrictMono f) :
    { ofColex := Finset.image f s } { ofColex := Finset.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 : Finset α} {t : Finset α} (hf : StrictMono f) :
    { ofColex := Finset.image f s } < { ofColex := Finset.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 : Finset.Colex α) => { ofColex := Finset.image f s.ofColex }
    Equations
    • Finset.Colex.instBoundedOrder = BoundedOrder.mk
    @[simp]
    theorem Finset.Colex.toColex_univ {α : Type u_1} [LinearOrder α] [Fintype α] :
    { ofColex := Finset.univ } =
    @[simp]
    theorem Finset.Colex.ofColex_top {α : Type u_1} [LinearOrder α] [Fintype α] :
    .ofColex = Finset.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
      theorem Finset.Colex.IsInitSeg.total {α : Type u_1} [LinearOrder α] {𝒜₁ : Finset (Finset α)} {𝒜₂ : Finset (Finset α)} {r : } (h₁ : Finset.Colex.IsInitSeg 𝒜₁ r) (h₂ : Finset.Colex.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.card elements and ending at s.

      Equations
      Instances For
        @[simp]
        theorem Finset.Colex.mem_initSeg {α : Type u_1} [LinearOrder α] {s : Finset α} {t : Finset α} [Fintype α] :
        t Finset.Colex.initSeg s s.card = t.card { ofColex := t } { ofColex := s }
        @[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𝒜 : Finset.Colex.IsInitSeg 𝒜 r) (h𝒜₀ : 𝒜.Nonempty) :
        ∃ (s : Finset α), s.card = r 𝒜 = Finset.Colex.initSeg s
        theorem Finset.Colex.isInitSeg_iff_exists_initSeg {α : Type u_1} [LinearOrder α] {𝒜 : Finset (Finset α)} {r : } [Fintype α] :
        Finset.Colex.IsInitSeg 𝒜 r 𝒜.Nonempty ∃ (s : Finset α), s.card = r 𝒜 = Finset.Colex.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 : Finset.Colex ) => ks.ofColex, n ^ k
        theorem Finset.geomSum_le_geomSum_iff_toColex_le_toColex {s : Finset } {t : Finset } {n : } (hn : 2 n) :
        ks, n ^ k kt, 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 : Finset } {t : Finset } {n : } (hn : 2 n) :
        is, n ^ i < it, 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 ) => is, n ^ i
        theorem Finset.lt_geomSum_of_mem {s : Finset } {n : } {a : } (hn : 2 n) (hi : a s) :
        a < is, n ^ i
        @[simp]
        theorem Finset.toFinset_bitIndices_twoPowSum (s : Finset ) :
        (∑ is, 2 ^ i).bitIndices.toFinset = s
        @[simp]
        theorem Finset.twoPowSum_toFinset_bitIndices (n : ) :
        in.bitIndices.toFinset, 2 ^ i = n
        @[simp]
        theorem Finset.equivBitIndices_apply (n : ) :
        Finset.equivBitIndices n = n.bitIndices.toFinset
        @[simp]
        theorem Finset.equivBitIndices_symm_apply (s : Finset ) :
        Finset.equivBitIndices.symm s = is, 2 ^ i

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem Finset.orderIsoColex_apply_ofColex (n : ) :
          (Finset.orderIsoColex n).ofColex = Finset.equivBitIndices n

          The equivalence Nat.equivBitIndices enumerates Finset in colexicographic order.

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