not_gf

Mathlib.SetTheory.PGame.Order

URI: https://scilib.ai/kg/mathlib#LE.le.not_gf

English

If x ≤ y, then not (y ⧏ x); i.e., ≤ implies the reverse not- lf relation.

Русский

Если x ≤ y, то не (y ⧏ x).

LaTeX

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

Lean4

theorem _root_.LE.le.not_gf {x y : PGame} : x ≤ y → ¬y ⧏ x :=
  not_lf.2

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

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

Разделы

Аффилиация

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