leftMovesOfStateAux — Mathlib

English

LeftMoves(ofStateAux n s hn) is equivalent to the set { t ∣ t ∈ l(s) }.

Русский

LeftMoves(ofStateAux n s hn) эквиваленто множеству {t | t ∈ l(s)}.

LaTeX

$$$ LeftMoves(ofStateAux(n,s,hn)) \cong \{ t \mid t \in l(s) \}$$$

Lean4

/-- The equivalence between `leftMoves` for a `PGame` constructed using `ofStateAux _ s _`, and
`L s`. -/
def leftMovesOfStateAux (n : ℕ) {s : S} (h : turnBound s ≤ n) : LeftMoves (ofStateAux n s h) ≃ { t // t ∈ l s } := by
  induction n <;> rfl

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