birthday_moveRight_lt — Mathlib

English

For any i in the right moves of x, the birthday of x.moveRight i is strictly smaller than the birthday of x.

Русский

Для любого i из правых ходов x, birthday (x.moveRight i) меньше birthday x.

LaTeX

$$$ \forall i \in x.RightMoves, (x.moveRight i).birthday < x.birthday $$$

Lean4

theorem birthday_moveRight_lt {x : PGame} (i : x.RightMoves) : (x.moveRight i).birthday < x.birthday := by cases x;
  rw [birthday]; exact lt_max_of_lt_right (lt_lsub _ i)

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