moveRight — Mathlib

English

If x ≡ y, then for every right move i of x there exists a right move j of y such that x.moveRight i ≡ y.moveRight j.

Русский

Если x ≡ y, то для каждого правого хода i x существует правый ход j y такой, что x.moveRight i ≡ y.moveRight j.

LaTeX

$$$ \forall x,y,\ x \equiv y \rightarrow \forall i : x.RightMoves, \exists j : y.RightMoves, x.moveRight i \equiv y.moveRight j $$$

Lean4

/-- If `x` and `y` are identical, then a right move of `x` is identical to some right move of `y`.
-/
theorem moveRight : ∀ {x y}, x ≡ y → ∀ i, ∃ j, x.moveRight i ≡ y.moveRight j
  | mk _ _ _ _, mk _ _ _ _, ⟨_, hr⟩, i => hr.1 i

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