isEmpty_rightMoves_mul — Mathlib

English

If the sum of products of moves is empty, then (x*y).RightMoves is empty.

Русский

Если сумма ходов пустая, то (x*y).RightMoves пусто.

LaTeX

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

Lean4

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

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