le_tsub_of_add_le_left

Mathlib.Algebra.Order.Sub.Defs

URI: https://scilib.ai/kg/mathlib#le_tsub_of_add_le_left

English

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

Русский

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

LaTeX

$$$b \le c - a$$$

Lean4

theorem le_tsub_of_add_le_left (h : a + b ≤ c) : b ≤ c - a :=
  Contravariant.AddLECancellable.le_tsub_of_add_le_left h

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

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

Разделы

Аффилиация

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