English
If x ≤ 0 and i is a left move of x, then the position after applying the right response to i remains ≤ 0.
Русский
Если x ≤ 0 и i — левый ход из x, то результат после правого ответа на i остаётся ≤ 0.
LaTeX
$$∀ {x}, (h : x ≤ 0) → ∀ {i}, i ∈ x.LeftMoves → (x.moveLeft i).moveRight (rightResponse h i) ≤ 0$$
Lean4
/-- Show that the response for right provided by `rightResponse` preserves the right-player-wins
condition. -/
theorem rightResponse_spec {x : PGame} (h : x ≤ 0) (i : x.LeftMoves) :
(x.moveLeft i).moveRight (rightResponse h i) ≤ 0 :=
Classical.choose_spec <| le_zero.1 h i