Commit 2022-05-05 09:52 4dfbcac3
View on Github →feat({data/{finset,set},order/filter}/pointwise): More basic API (#13899)
More basic lemmas about pointwise operations on set
/finset
/filter
. Also make the three APIs more consistent with each other.