ltTrichotomy_lt

Mathlib.Order.Basic

URI: https://scilib.ai/kg/mathlib#ltTrichotomy_lt

English

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

Русский

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

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru