le_of_lf

Mathlib.SetTheory.Surreal.Basic

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

English

If x and y are numeric and x ⧏ y, then not (y ⧏ x).

Русский

Если x и y числовые и x ⧏ y, то не выполняется y ⧏ x.

LaTeX

$$$x \mathbf{LF} y \Rightarrow \neg (y \mathbf{LF} x)$$$

Lean4

theorem le_of_lf {x y : PGame} (h : x ⧏ y) (ox : Numeric x) (oy : Numeric y) : x ≤ y :=
  not_lf.1 (lf_asymm ox oy h)

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

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

Разделы

Аффилиация

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