Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-17 10:14 1c56a8de

View on Github →

feat(order/well_founded_set): Antichains in a partial well order are finite (#11286) and when the relation is reflexive and symmetric, it's actually an equivalent condition.

Estimated changes