English
The three-way case distinction ltByCases selects the first branch when x < y; more precisely, if x < y then the value is h1 h where h1 is the x<y-branch and h is its witness.
Русский
Разделение по трём случаям ltByCases выбирает первую ветвь, когда x < y; более точно, если x < y, то значение равно h1 h, где h1 — это ветвь для x < y, и h — её доказательство.
LaTeX
$$$ ltByCases(x, y, h_1, h_2, h_3) = h_1(h) \\\\; (\\text{при } h: x < y) $$$
Lean4
@[deprecated lt_trichotomy (since := "2025-04-21")]
theorem ltByCases_lt (h : x < y) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} : ltByCases x y h₁ h₂ h₃ = h₁ h :=
dif_pos h
