Commit 2020-11-23 13:47 13b9478e

View on Github →

feat(combinatorics/colex): introduce colexicographical order (#4858) We define the colex ordering for finite sets, and give a couple of important lemmas and properties relating to it. Part of #2770, in order to prove the Kruskal-Katona theorem.

Estimated changes

Created src/combinatorics/colex.lean

added theorem colex.eq_iff

added theorem colex.forall_lt_of_colex_lt_of_forall_lt

added theorem colex.hom

added theorem colex.hom_fin

added theorem colex.le_def

added theorem colex.le_trans

added theorem colex.lt_def

added theorem colex.lt_singleton_iff_mem_lt

added theorem colex.lt_trans

added theorem colex.lt_trichotomy

added theorem colex.mem_le_of_singleton_le

added theorem colex.sdiff_lt_sdiff_iff_lt

added theorem colex.singleton_lt_iff_lt

added theorem colex.sum_pow_two_lt_iff_lt

added def finset.colex

added def finset.to_colex

added theorem nat.sum_pow_two_lt