sub — Mathlib

English

If x1 ≡ x2 and y1 ≡ y2, then x1 - y1 ≡ x2 - y2.

Русский

Если x1 эквивалентен x2 и y1 эквивалентен y2, то x1 − y1 эквивалентен x2 − y2.

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 sub {x₁ x₂ y₁ y₂ : PGame.{u}} (hx : x₁ ≡ x₂) (hy : y₁ ≡ y₂) : x₁ - y₁ ≡ x₂ - y₂ :=
  hx.add hy.neg

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