ltTrichotomy_eq — Mathlib

English

If not x < y, then ltTrichotomy x y p q r equals the appropriate case: if y < x then r else q.

Русский

Если не выполняется x < y, то ltTrichotomy x y p q r принимает соответствующий случай: если y < x тогда r, иначе q.

LaTeX

$$$ \\lnot (x < y) \\Rightarrow ltTrichotomy(x, y, p, q, r) = \\text{if } y < x \\text{ then } r \\text{ else } q $$$

Lean4

@[deprecated lt_trichotomy (since := "2025-04-21")]
theorem ltTrichotomy_eq (h : x = y) : ltTrichotomy x y p q r = q :=
  ltByCases_eq h

Похожие утверждения