Commit 2020-07-25 05:30 2d29f80a

View on Github →

feat(data/finsupp): lattice structure on finsupp (#3335) adds facts about order_isos respecting lattice operations defines lattice structures on finsupps to N constructs an order_iso out of finsupp.to_multiset

Estimated changes

Modified src/algebra/ordered_group.lean

Created src/data/finsupp/lattice.lean

added theorem finsupp.bot_eq_zero

added theorem finsupp.disjoint_iff

added theorem finsupp.inf_apply

added theorem finsupp.le_def

added theorem finsupp.monotone_to_fun

added theorem finsupp.of_multiset_strict_mono

added def finsupp.order_embedding_to_fun

added theorem finsupp.order_embedding_to_fun_apply

added def finsupp.order_iso_multiset

added theorem finsupp.order_iso_multiset_apply

added theorem finsupp.order_iso_multiset_symm_apply

added theorem finsupp.sup_apply

added theorem finsupp.support_inf

added theorem finsupp.support_sup