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
: ifs < t
in colex, and everything int
is< a
, then everything ins
is< a
. This confirms the idea that an enumeration under colex will exhaust all sets using elements< a
before allowinga
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 #
Tags #
colex, colexicographic, binary
Type synonym of Finset α
equipped with the colexicographic order rather than the inclusion
order.
- toColex :: (
- ofColex : Finset α
ofColex
is the "identity" function betweenFinset.Colex α
andFinset α
. - )
Instances For
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 }
Equations
- Finset.Colex.instPartialOrder = PartialOrder.mk ⋯
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.
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.
Equations
- Finset.Colex.instOrderBot = OrderBot.mk ⋯
If s ≤ t
in colex, and all elements in t
are small, then all elements in s
are small.
If s ≤ t
in colex, and all elements in t
are small, then all elements in s
are small.
s < {a}
in colex iff all elements of s
are strictly less than a
.
{a} ≤ s
in colex iff s
contains an element greated than or equal to a
.
Colex is an extension of the base order.
Colex is an extension of the base order.
Equations
- s.instDecidableEq t = decidable_of_iff' (s.ofColex = t.ofColex) ⋯
Equations
- s.instDecidableLE t = decidable_of_iff' (∀ ⦃a : α⦄, a ∈ s.ofColex → a ∉ t.ofColex → ∃ b ∈ t.ofColex, b ∉ s.ofColex ∧ a ≤ b) ⋯
Equations
- Finset.Colex.instDecidableLT = decidableLTOfDecidableLE
The colexigraphic order is insensitive to removing the same elements from both sets.
The colexigraphic order is insensitive to removing the same elements from both sets.
Equations
- Finset.Colex.instLinearOrder = LinearOrder.mk ⋯ Finset.Colex.instDecidableLE decidableEqOfDecidableLE Finset.Colex.instDecidableLT ⋯ ⋯ ⋯
Strictly monotone functions preserve the colex ordering.
Strictly monotone functions preserve the colex ordering.
Initial segments #
𝒜
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
Initial segments are nested in some way. In particular, if they're the same size they're equal.
The initial segment of the colexicographic order on sets with s.card
elements and ending at
s
.
Equations
- Finset.Colex.initSeg s = Finset.filter (fun (t : Finset α) => s.card = t.card ∧ { ofColex := t } ≤ { ofColex := s }) Finset.univ
Instances For
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.
The equivalence Nat.equivBitIndices
enumerates Finset ℕ
in colexicographic order.
Equations
- One or more equations did not get rendered due to their size.