rightResponse_spec — Mathlib

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

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