Theorem Pi.isTrichotomous_lex

Modification history

2026-02-06 11:53

Mathlib/Order/PiLex.lean

chore(Order/Defs/Unbundled): deprecate `IsTrichotomous` in favor of core's `Std.Trichotomous` (#34349)

Deleted Pi.isTrichotomous_lex View on Github →

2022-12-20 13:42

Mathlib/Data/Pi/Lex.lean

feat: port Data.Pi.Lex (#1104) …

Added Pi.isTrichotomous_lex View on Github →