mathlib3
f55d3524 - feat(order/filter/n_ary): Binary and ternary maps of filters (#13062)

Commit
3 years ago
feat(order/filter/n_ary): Binary and ternary maps of filters (#13062) Define `filter.map₂` and `filter.map₃`, the binary and ternary maps of filters.
Author
Parents
Loading