ltTrichotomy_gt

Mathlib.Order.Basic

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

English

If x = y, then ltTrichotomy x y p q r equals q, i.e., the middle branch is taken.

Русский

Если x = y, то ltTrichotomy x y p q r равно q, то есть берётся средняя ветвь.

LaTeX

$$$ x = y \\Rightarrow ltTrichotomy(x, y, p, q, r) = q $$$

Lean4

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

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

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

Разделы

Аффилиация

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