not_gt — Mathlib

English

Let x, y be elements of the LF-ordered game class. If x ⧏ y, then y is not strictly less than x (i.e., ¬(y < x)).

Русский

Пусть x, y — элементы множества игр. Если x ⧏ y, то y не меньше x в строгом смысле, то есть ¬(y < x).

LaTeX

$$$\forall x,y \in \mathrm{PGame},\ x \mathrel{⧏} y \rightarrow \neg (y < x)$$$

Lean4

theorem not_gt {x y : PGame} (h : x ⧏ y) : ¬y < x := fun h' => h.not_ge h'.le

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