Commit 2023-02-04 10:30 acdd22b2

View on Github →

feat: port Combinatorics.Colex (#1926)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Colex.lean

added theorem Colex.colex_le_of_subset

added theorem Colex.colex_lt_of_sSubset

added theorem Colex.empty_toColex_le

added theorem Colex.empty_toColex_lt

added theorem Colex.eq_iff

added theorem Colex.forall_lt_of_colex_lt_of_forall_lt

added theorem Colex.hom_fin_le_iff

added theorem Colex.hom_fin_lt_iff

added theorem Colex.hom_le_iff

added theorem Colex.hom_lt_iff

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_le_sdiff_iff_le

added theorem Colex.sdiff_lt_sdiff_iff_lt

added theorem Colex.singleton_le_iff_le

added theorem Colex.singleton_lt_iff_lt

added theorem Colex.sum_two_pow_le_iff_lt

added theorem Colex.sum_two_pow_lt_iff_lt

added def Colex.toColexRelHom

added def Finset.Colex

added def Finset.toColex

added theorem Nat.sum_two_pow_lt