Commit 2024-01-12 12:47 e4eb07af

View on Github →

feat(Order/Basic): Add ltByCases API (#9114) I noticed that ltByCases doesn't have any API, and it would be useful to have some when working trichotomously, especially if one wishes to define things trichotomously. A non-dependent version is also defined.

Estimated changes

added theorem ltByCases_comm
added theorem ltByCases_congr
added theorem ltByCases_eq
added theorem ltByCases_eq_iff
added theorem ltByCases_gt
added theorem ltByCases_lt
added theorem ltByCases_ne
added theorem ltByCases_not_gt
added theorem ltByCases_not_lt
added theorem ltByCases_rec
added theorem ltTrichotomy_comm
added theorem ltTrichotomy_congr
added theorem ltTrichotomy_eq
added theorem ltTrichotomy_eq_iff
added theorem ltTrichotomy_gt
added theorem ltTrichotomy_lt
added theorem ltTrichotomy_ne
added theorem ltTrichotomy_not_gt
added theorem ltTrichotomy_not_lt
added theorem ltTrichotomy_self