rightMovesOfStateAux — Mathlib

English

RightMoves(ofStateAux n s hn) corresponds to { t ∈ r(s) }.

Русский

RightMoves(ofStateAux n s hn) соответствует { t ∈ r(s) }.

LaTeX

$$$ RightMoves(ofStateAux(n,s,hn)) \cong \{ t \mid t \in r(s) \}$$$

Lean4

/-- The equivalence between `rightMoves` for a `PGame` constructed using `ofStateAux _ s _`, and
`R s`. -/
def rightMovesOfStateAux (n : ℕ) {s : S} (h : turnBound s ≤ n) : RightMoves (ofStateAux n s h) ≃ { t // t ∈ r s } := by
  induction n <;> rfl

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