leftMoves_mul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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