moveLeft — Mathlib

English

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

Русский

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

LaTeX

$$$ \forall x,y,\ x \equiv y \rightarrow \forall i : x.LeftMoves, \exists j : y.LeftMoves, x.moveLeft i \equiv y.moveLeft j $$$

Lean4

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

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