Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-17 04:40 08931580

View on Github →

refactor(order/rel_classes): redefine is_well_order in terms of is_well_founded (#15729) We redefine is_well_order in terms of is_well_founded, and remove the redundant is_irrefl assumption in the process. This also replaces is_well_order.wf with is_well_founded.wf.

Estimated changes