English
If two ordered pairs have corresponding order relations (x<y) ↔ (x'<y') and (y<x) ↔ (y'<x'), and the responses on the branches match appropriately, then the two ltByCases expressions are equal.
Русский
Если два упорядоченных пары имеют соответствующие отношения порядка и соответствия веток, то их значения ltByCases совпадают.
LaTeX
$$$ ltByCases(x, y, h_1, h_2, h_3) = ltByCases(x', y', h_1', h_2', h_3') $$$
Lean4
@[deprecated lt_trichotomy (since := "2025-04-21")]
theorem ltByCases_eq_iff {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} {p : P} :
ltByCases x y h₁ h₂ h₃ = p ↔ (∃ h, h₁ h = p) ∨ (∃ h, h₂ h = p) ∨ (∃ h, h₃ h = p) :=
by
refine ltByCases x y (fun h => ?_) (fun h => ?_) (fun h => ?_)
· simp only [ltByCases_lt, exists_prop_of_true, h, h.not_gt, not_false_eq_true, exists_prop_of_false, or_false, h.ne]
·
simp only [h, lt_self_iff_false, ltByCases_eq, not_false_eq_true, exists_prop_of_false, exists_prop_of_true,
or_false, false_or]
· simp only [ltByCases_gt, exists_prop_of_true, h, h.not_gt, not_false_eq_true, exists_prop_of_false, false_or, h.ne']
