Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-26 11:31 8fcb820b

View on Github →

feat(order/filter/basic): add filter.has_basis.bInter_mem (#15661) Use it to golf a few proofs.

Estimated changes