Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-31 14:15 bc5e0081

View on Github →

feat(data/dfinsupp/order): Pointwise order on finitely supported dependent functions (#11138) This defines the pointwise order on Π₀ i, α i, in very much the same way as in data.finsupp.order. It also moves data.dfinsupp to data.dfinsupp.basic.

Estimated changes

added theorem dfinsupp.coe_fn_mono
added theorem dfinsupp.coe_tsub
added theorem dfinsupp.disjoint_iff
added theorem dfinsupp.inf_apply
added theorem dfinsupp.le_def
added theorem dfinsupp.le_iff'
added theorem dfinsupp.le_iff
added theorem dfinsupp.single_le_iff
added theorem dfinsupp.single_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