sub_add_cancel_right — Mathlib

English

Let a be an element of the extended real numbers and b a real number. Then b − (a + b) = −a.

Русский

Пусть a принадлежит расшіренным вещественным числам, а b — действительное число. Тогда b − (a + b) = −a.

LaTeX

$$$\forall a \in \mathrm{EReal}, \forall b \in \mathbb{R},\quad b - (a + b) = -a$$$

Lean4

theorem sub_add_cancel_right {a : EReal} {b : Real} : b - (a + b) = -a :=
  by
  cases a <;> norm_cast
  exact _root_.sub_add_cancel_right _ _

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