le_add_tsub

Mathlib.Algebra.Order.Sub.Defs

URI: https://scilib.ai/kg/mathlib#AddLECancellable.le_add_tsub

English

If b is cancellable, then a ≤ a + b − b.

Русский

Если b является допускающим отмену, то a ≤ a + b − b.

LaTeX

$$$a \le a + b - b$$$

Lean4

protected theorem le_add_tsub (hb : AddLECancellable b) : a ≤ a + b - b :=
  by
  rw [add_comm]
  exact hb.le_add_tsub_swap

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

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

Разделы

Аффилиация

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