leftMovesOfState — Mathlib

English

The left-move structure of a game built from a state s corresponds to l(s).

Русский

Структура левых ходов игры, построенной из состояния s, соответствует l(s).

LaTeX

$$$ leftMoves( ofState(s) ) \cong \{ t \mid t \in l(s) \}$$$

Lean4

/-- The equivalence between `leftMoves` for a `PGame` constructed using `ofState s`, and `l s`. -/
def leftMovesOfState (s : S) : LeftMoves (ofState s) ≃ { t // t ∈ l s } :=
  leftMovesOfStateAux _ _

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