isEmpty_leftMoves_mul — Mathlib

English

If the sum of products of moves is empty, then (x*y).LeftMoves is empty; i.e., no left moves arise in the product.

Русский

Если сумма произведений ходов пустая, то (x*y).LeftMoves пусто; то есть в произведении нет левых ходов.

LaTeX

$$$$IsEmpty((x*y).LeftMoves) \\quad \\text{given } IsEmpty(x^L \\times y^L \\oplus x^R \\times y^R).$$$$

Lean4

instance isEmpty_leftMoves_mul (x y : PGame.{u}) [IsEmpty (x.LeftMoves × y.LeftMoves ⊕ x.RightMoves × y.RightMoves)] :
    IsEmpty (x * y).LeftMoves := by
  cases x
  cases y
  assumption

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