Theorem isChain_univ_iff

Modification history

2026-02-06 11:53
Mathlib/Order/Preorder/Chain.lean
chore(Order/Defs/Unbundled): deprecate `IsTrichotomous` in favor of core's `Std.Trichotomous` (#34349)
Modified isChain_univ_iffView on Github →
2022-12-29 00:36
Mathlib/Order/Chain.lean
feat: port `Order.Chain` (#1205) …
Added isChain_univ_iffView on Github →