ltTrichotomy_comm — Mathlib

English

Equivalently, the value ltTrichotomy x y p q r equals s if and only if s arises from the corresponding branch based on the order (x<y, x=y, y<x).

Русский

Эквивалентно: значение ltTrichotomy x y p q r равно s тогда и только тогда, когда s получается из соответствующей ветви в зависимости от порядка (x<y, x=y, y<x).

LaTeX

$$$ Eq(ltTrichotomy x y p q r, s) \\iff (x < y \\land p = s) \\lor (x = y \\land q = s) \\lor (y < x \\land r = s) $$$

Lean4

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

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