lt_or_equiv_or_gt

Mathlib.SetTheory.Surreal.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$x < y ∨ (x ≈ y) ∨ y < x$$

Lean4

theorem lt_or_equiv_or_gt {x y : PGame} (ox : Numeric x) (oy : Numeric y) : x < y ∨ (x ≈ y) ∨ y < x :=
  ((lf_or_equiv_or_gf x y).imp fun h => h.lt ox oy) <| Or.imp_right fun h => h.lt oy ox

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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