neg_add — Mathlib

English

Negation distributes over addition: the negation of a sum is the sum of negations, i.e., −(x+y) = −x + −y.

Русский

Отрицание распределяется над сложением: −(x+y) = −x + −y.

LaTeX

$$$ -(x+y) = -x + -y $$$

Lean4

/-- `-(x + y)` has exactly the same moves as `-x + -y`. -/
protected theorem neg_add (x y : PGame) : -(x + y) = -x + -y :=
  match x, y with
  | mk xl xr xL xR, mk yl yr yL yR => by
    refine ext rfl rfl ?_ ?_ <;>
      · rintro (i | i) _ ⟨rfl⟩
        · exact PGame.neg_add _ _
        · simpa [Equiv.refl, mk_add_moveLeft, mk_add_moveRight] using PGame.neg_add _ _
termination_by (x, y)

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