leftResponse_spec — Mathlib

English

If 0 ≤ x and j is a right move of x, then 0 ≤ the left response after j.

Русский

Если 0 ≤ x и j — правый ход из x, то 0 ≤ левая реакция после j.

LaTeX

$$∀ {x}, (h : 0 ≤ x) → ∀ {j}, j ∈ x.RightMoves → 0 ≤ (x.moveRight j).moveLeft (leftResponse h j)$$

Lean4

/-- Show that the response for left provided by `leftResponse` preserves the left-player-wins
condition. -/
theorem leftResponse_spec {x : PGame} (h : 0 ≤ x) (j : x.RightMoves) :
    0 ≤ (x.moveRight j).moveLeft (leftResponse h j) :=
  Classical.choose_spec <| zero_le.1 h j

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