isEmpty_leftMoves_add — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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