Def IsChain.linearOrder

Modification history

2026-09-05 15:48
Mathlib/Order/Preorder/Chain.lean
feat(Order/OrderIsoNat): every chain is finite when `<` and `>` are well-founded (#42633) …
Modified IsChain.linearOrderView on Github →
2026-06-21 22:46
Mathlib/Order/Preorder/Chain.lean
feat: monotone function `Cardinal → α` is eventually constant (#37344)
Added IsChain.linearOrderView on Github →