insertRight_le — Mathlib

English

Adding a new Right option cannot worsen Right's position; insertRight x x' ≤ x.

Русский

Добавление нового правого хода не ухудшает положение Правого; insertRight x x' ≤ x.

LaTeX

$$$insertRight\; x\; x' \le x$$$

Lean4

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

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