Commit 2023-02-06 07:04 46f5661d

View on Github →

feat: port Data.Dfinsupp.Order (#1942)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Dfinsupp/Order.lean

added theorem Dfinsupp.add_eq_zero_iff

added theorem Dfinsupp.coeFn_mono

added theorem Dfinsupp.coe_tsub

added theorem Dfinsupp.inf_apply

added theorem Dfinsupp.le_def

added theorem Dfinsupp.le_iff'

added theorem Dfinsupp.le_iff

added def Dfinsupp.orderEmbeddingToFun

added theorem Dfinsupp.orderEmbeddingToFun_apply

added theorem Dfinsupp.single_le_iff

added theorem Dfinsupp.single_tsub

added theorem Dfinsupp.subset_support_tsub

added theorem Dfinsupp.sup_apply

added theorem Dfinsupp.support_inf

added theorem Dfinsupp.support_sup

added theorem Dfinsupp.support_tsub

added theorem Dfinsupp.tsub_apply