neg_sub — Mathlib

English

For x, y ∈ EReal with not (x = ⊥ and y = ⊥) and not (x = ⊤ and y = ⊤), -(x - y) = -x + y.

Русский

Для x, y ∈ EReal, если не (x = ⊥ и y = ⊥) и не (x = ⊤ и y = ⊤), то -(x - y) = -x + y.

LaTeX

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

Lean4

theorem neg_sub {x y : EReal} (h1 : x ≠ ⊥ ∨ y ≠ ⊥) (h2 : x ≠ ⊤ ∨ y ≠ ⊤) : -(x - y) = -x + y := by
  rw [sub_eq_add_neg, neg_add _ _, sub_eq_add_neg, neg_neg] <;> simp_all

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