Commit 2025-01-20 16:09 dfa76e7f

feat(Order/Chain): adapt linear order lemmas to chains (#20757) Add a series of lemmas for chains in a preorder. Each of these are true in a linear order, but remain true under the weaker assumption that both elements are in a chain. Used in the disproof of the Aharoni–Korman conjecture, https://github.com/leanprover-community/mathlib4/pull/20082.