not_ge

Mathlib.SetTheory.PGame.Order

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

English

If x ⧏ y then not y ≤ x; i.e., lf-advances imply a strict separation from the bound.

Русский

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

LaTeX

$$$x \;⧏\; y \rightarrow \neg (y \le x)$$$

Lean4

theorem not_ge {x y : PGame} : x ⧏ y → ¬y ≤ x :=
  id

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

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

Разделы

Аффилиация

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