Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-17 19:54 1fbef63a

View on Github →

feat(order/filter): add two lemmas (#11519) Two easy lemmas (from the sphere eversion project) and some minor style changes.

Estimated changes