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
.