le_iff_forall_lt — Mathlib

English

If LeftMoves and RightMoves are empty, then x is numeric.

Русский

Если LeftMoves и RightMoves пусты, то x числовая.

LaTeX

$$Numeric x$$

Lean4

/-- Definition of `x ≤ y` on numeric pre-games, in terms of `<` -/
theorem le_iff_forall_lt {x y : PGame} (ox : x.Numeric) (oy : y.Numeric) :
    x ≤ y ↔ (∀ i, x.moveLeft i < y) ∧ ∀ j, x < y.moveRight j := by
  refine le_iff_forall_lf.trans (and_congr ?_ ?_) <;> refine forall_congr' fun i => lf_iff_lt ?_ ?_ <;>
    apply_rules [Numeric.moveLeft, Numeric.moveRight]

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