ltTrichotomy — Mathlib

English

If x < y, then ltTrichotomy x y p q r equals p, selecting the first branch.

Русский

Если x < y, то ltTrichotomy x y p q r выбирает первую ветвь, давая p.

LaTeX

$$$ ltTrichotomy(x, y, p, q, r) = p \\; (\\text{при } x < y) $$$

Lean4

/-- Perform a case-split on the ordering of `x` and `y` in a decidable linear order,
non-dependently. -/
@[deprecated lt_trichotomy (since := "2025-04-21")]
abbrev ltTrichotomy (x y : α) (p q r : P) :=
  ltByCases x y (fun _ => p) (fun _ => q) (fun _ => r)

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