lf_iff_lt

Mathlib.SetTheory.Surreal.Basic

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.lf_iff_lt

English

For numeric x,y, either x < y, or x ≈ y, or y < x.

Русский

Для числовых x,y либо x < y, либо x ≈ y, либо y < x.

LaTeX

$$$x < y \; \lor\; x \approx y \; \lor\; y < x$$$

Lean4

theorem lf_iff_lt {x y : PGame} (ox : Numeric x) (oy : Numeric y) : x ⧏ y ↔ x < y :=
  ⟨fun h => h.lt ox oy, lf_of_lt⟩

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

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

Разделы

Аффилиация

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