le_of_forall_lf — Mathlib

English

Let x and y be pre-games. If every Left option of x is strictly less than y and every Right option of y is strictly greater than x, then x is less than or equal to y in the game ordering.

Русский

Пусть x и y — предигры. Если каждая левая ходовая позиция x строго меньше y и каждая правая ходовая позиция y строго больше x, то x ≤ y в порядке игр.

LaTeX

$$$\\\\forall x,y\\\\in \\\\mathrm{PGame},\\\\(\\\\forall i, x.moveLeft(i) \\\\mathrm{⧏}\\\\ y) \\\\land \\\\(\\\\forall j, x \\\\mathrm{⧏}\\\\ y.moveRight(j) \\\\Rightarrow x \\\\le y$$$

Lean4

theorem le_of_forall_lf {x y : PGame} (h₁ : ∀ i, x.moveLeft i ⧏ y) (h₂ : ∀ j, x ⧏ y.moveRight j) : x ≤ y :=
  le_iff_forall_lf.2 ⟨h₁, h₂⟩

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