add_sub_cancel_left

Mathlib.Data.EReal.Operations

URI: https://scilib.ai/kg/mathlib#EReal.add_sub_cancel_left

English

b + a − b = a for all a ∈ EReal, b ∈ Real.

Русский

b + a − b = a для всех a ∈ EReal, b ∈ Real.

LaTeX

$$$$b + a - b = a.$$$$

Lean4

theorem add_sub_cancel_left {a : EReal} {b : Real} : b + a - b = a := by rw [add_comm, EReal.add_sub_cancel_right]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru