Commit 2021-07-20 16:22 6ac3059b

View on Github →

feat(combinatorics/colex): golf and generalise (#8301) Miscellaneous fixes about colex: Gives le versions of some lt lemmas, fixes a TODO, restores some names etc.

Estimated changes

Modified src/combinatorics/colex.lean

added theorem colex.colex_le_of_subset

added theorem colex.colex_lt_of_ssubset

added theorem colex.empty_to_colex_le

added theorem colex.empty_to_colex_lt

deleted theorem colex.hom

deleted theorem colex.hom_fin

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

modified theorem colex.lt_singleton_iff_mem_lt

added theorem colex.sdiff_le_sdiff_iff_le

added theorem colex.singleton_le_iff_le

deleted theorem colex.sum_sq_lt_iff_lt

added theorem colex.sum_two_pow_le_iff_lt

added theorem colex.sum_two_pow_lt_iff_lt

added def colex.to_colex_rel_hom

deleted theorem nat.sum_sq_lt

added theorem nat.sum_two_pow_lt