birthday_moveLeft_lt — Mathlib

English

For any i in the left moves of x, the birthday of x.moveLeft i is strictly smaller than the birthday of x.

Русский

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

LaTeX

$$$ \forall i \in x.LeftMoves, (x.moveLeft i).birthday < x.birthday $$$

Lean4

theorem birthday_moveLeft_lt {x : PGame} (i : x.LeftMoves) : (x.moveLeft i).birthday < x.birthday := by cases x;
  rw [birthday]; exact lt_max_of_lt_left (lt_lsub _ i)

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