le_insertLeft — Mathlib

English

Adding a new Left option cannot worsen Left's position; x ≤ insertLeft x x'.

Русский

Добавление нового левого хода не ухудшает положение Левой стороны; x ≤ insertLeft x x'.

LaTeX

$$$x \le insertLeft\; x\; x'$$

Lean4

/-- A new left option cannot hurt Left. -/
theorem le_insertLeft (x x' : PGame) : x ≤ insertLeft x x' :=
  by
  rw [le_def]
  constructor
  · intro i
    left
    rcases x with ⟨xl, xr, xL, xR⟩
    simp only [insertLeft, leftMoves_mk, moveLeft_mk, Sum.exists, Sum.elim_inl]
    left
    use i
  · intro j
    right
    rcases x with ⟨xl, xr, xL, xR⟩
    simp only [rightMoves_mk, moveRight_mk, insertLeft]
    use j

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