neg_add — Mathlib

English

If x, y ∈ EReal and not (x = ⊥ and y = ⊤) and not (x = ⊤ and y = ⊥), then -(x + y) = -x - y.

Русский

Если x, y ∈ EReal и не выполняются пары (x = ⊥, y = ⊤) или (x = ⊤, y = ⊥), то -(x + y) = -x - y.

LaTeX

$$$$\neg (x=\bot \land y=\top) \land \neg (x=\top \land y=\bot) \Rightarrow -(x+y) = -x - y.$$$$

Lean4

theorem neg_add {x y : EReal} (h1 : x ≠ ⊥ ∨ y ≠ ⊤) (h2 : x ≠ ⊤ ∨ y ≠ ⊥) : -(x + y) = -x - y :=
  by
  induction x <;> induction y <;> try tauto
  rw [← coe_add, ← coe_neg, ← coe_neg, ← coe_sub, neg_add']

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