mathlib3
9cf6766f - feat(order/filter/pi): define `filter.pi` and prove some properties (#10323)

Commit

4 years ago

feat(order/filter/pi): define `filter.pi` and prove some properties (#10323)

Author

urkud

urkud

Parents

Loading