ltTrichotomy_not_lt — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[deprecated lt_trichotomy (since := "2025-04-21")]
theorem ltTrichotomy_not_lt (h : ¬x < y) : ltTrichotomy x y p q r = if y < x then r else q :=
  ltByCases_not_lt h

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