ltByCases — Mathlib

English

In a decidable linear order, one can perform a three-way case split according to x < y, x = y, or y < x.

Русский

В разрешимом линейном порядке существует трипоточное разбиение по x < y, x = y или y < x.

LaTeX

$$$ (x < y) \\lor (x = y) \\lor (y < x) $$$

Lean4

/-- Perform a case-split on the ordering of `x` and `y` in a decidable linear order. -/
@[deprecated lt_trichotomy (since := "2025-04-21")]
def ltByCases (x y : α) {P : Sort*} (h₁ : x < y → P) (h₂ : x = y → P) (h₃ : y < x → P) : P :=
  if h : x < y then h₁ h else if h' : y < x then h₃ h' else h₂ (le_antisymm (le_of_not_gt h') (le_of_not_gt h))

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