isEmpty_rightMoves_add — Mathlib

English

If the right moves of x and y are empty, then the right moves of x + y are empty.

Русский

Если правые ходы x и y пусты, то и правые ходы суммы x + y пусты.

LaTeX

$$$\\operatorname{IsEmpty}(x.RightMoves) \\land \\operatorname{IsEmpty}(y.RightMoves) \\Rightarrow \\operatorname{IsEmpty}((x+y).RightMoves)$$$

Lean4

instance isEmpty_rightMoves_add (x y : PGame.{u}) [IsEmpty x.RightMoves] [IsEmpty y.RightMoves] :
    IsEmpty (x + y).RightMoves := by
  cases x
  cases y
  apply isEmpty_sum.2 ⟨_, _⟩
  assumption'

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