add — Mathlib

English

If x₁ ≡ x₂ and y₁ ≡ y₂, then x₁ + y₁ ≡ x₂ + y₂.

Русский

Если x₁ эквивалентен x₂ и y₁ эквивалентен y₂, то x₁ + y₁ эквивалентно x₂ + y₂.

LaTeX

$$$ x_1 \equiv x_2 \;\land\; y_1 \equiv y_2 \Rightarrow x_1 + y_1 \equiv x_2 + y_2 $$$

Lean4

/-- If `w` has the same moves as `x` and `y` has the same moves as `z`,
then `w + y` has the same moves as `x + z`. -/
theorem add {x₁ x₂ y₁ y₂ : PGame.{u}} (hx : x₁ ≡ x₂) (hy : y₁ ≡ y₂) : x₁ + y₁ ≡ x₂ + y₂ :=
  hx.add_right.trans hy.add_left

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