English
If the order relations between two pairs are correspondingly equivalent, then the two trichotomy expressions are equal.
Русский
Если порядка между двумя парами соответствующим образом эквивалентны, то два выражения тричитотомии равны.
LaTeX
$$$ ltTrichotomy x y p q r = ltTrichotomy x' y' p' q' r' $$$
Lean4
@[deprecated lt_trichotomy (since := "2025-04-21")]
theorem ltTrichotomy_congr {x' y' : α} {p' q' r' : P} (ltc : (x < y) ↔ (x' < y')) (gtc : (y < x) ↔ (y' < x'))
(hh'₁ : x' < y' → p = p') (hh'₂ : x' = y' → q = q') (hh'₃ : y' < x' → r = r') :
ltTrichotomy x y p q r = ltTrichotomy x' y' p' q' r' :=
ltByCases_congr ltc gtc hh'₁ hh'₂ hh'₃
