le_of_forall_lt — Mathlib

English

If for all i, x.moveLeft i < y and for all j, x < y.moveRight j, then x ≤ y.

Русский

Если для всех i выполняется x.moveLeft i < y и для всех j выполняется x < y.moveRight j, то x ≤ y.

LaTeX

$$$$ (\\\\forall i, x.moveLeft i < y) \\\\land (\\\\forall j, x < y.moveRight j) \\\\Rightarrow x \\\\le y. $$$$

Lean4

/-- This special case of `PGame.le_of_forall_lf` is useful when dealing with surreals, where `<` is
preferred over `⧏`. -/
theorem le_of_forall_lt {x y : PGame} (h₁ : ∀ i, x.moveLeft i < y) (h₂ : ∀ j, x < y.moveRight j) : x ≤ y :=
  le_of_forall_lf (fun i => (h₁ i).lf) fun i => (h₂ i).lf

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