Commit 2025-01-16 16:08 78512f52
View on Github →feat(Order/WellFoundedSet): add convenience constructors for IsWF and IsPWO for WellFoundedLT types (#20752)
A useful lemma from the disproof of the Aharoni–Korman conjecture, https://github.com/leanprover-community/mathlib4/pull/20082.
While these are easy to inline, they are hard to discover for an end user, since WellFoundedLT is never mentioned in this file. As such, this change improves discoverability, especially with exact?.