insertRight_numeric — Mathlib

English

If x and x' are numeric and x ≤ x', then insertRight(x, x') is numeric.

Русский

Если x и x' числовые и x ≤ x', то вставка справа x' к x числовая.

LaTeX

$$$(Numeric(x) \land Numeric(x') \land x \le x') \Rightarrow Numeric(x.insertRight(x'))$$$

Lean4

/-- Inserting a larger numeric right option into a numeric game results in a numeric game. -/
theorem insertRight_numeric {x x' : PGame} (x_num : x.Numeric) (x'_num : x'.Numeric) (h : x ≤ x') :
    (insertRight x x').Numeric :=
  by
  rw [← neg_neg (x.insertRight x'), ← neg_insertLeft_neg]
  apply Numeric.neg
  exact insertLeft_numeric (Numeric.neg x_num) (Numeric.neg x'_num) (neg_le_neg_iff.mpr h)

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