rightMoves_mul — Mathlib

English

The RightMoves of the product x*y are the disjoint union of the products of right moves and left moves and of left moves and right moves: (x*y).RightMoves = (x.LeftMoves × y.RightMoves) ⊕ (x.RightMoves × y.LeftMoves).

Русский

Множество правых ходов произведения x*y равно объединению пар (x.LeftMoves × y.RightMoves) и (x.RightMoves × y.LeftMoves).

LaTeX

$$$ (x * y).RightMoves = (x.LeftMoves \times y.RightMoves) \oplus (x.RightMoves \times y.LeftMoves) $$$

Lean4

theorem rightMoves_mul :
    ∀ x y : PGame.{u}, (x * y).RightMoves = (x.LeftMoves × y.RightMoves ⊕ x.RightMoves × y.LeftMoves)
  | ⟨_, _, _, _⟩, ⟨_, _, _, _⟩ => rfl

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