tsub_le_self

Mathlib.Algebra.Order.Sub.Basic

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

English

For any a,b in a canonically ordered additive monoid, a − b ≤ a.

Русский

Пусть a,b ∈ канонически упорядоченной аддитивной полугруппы; тогда a − b ≤ a.

LaTeX

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

Lean4

theorem tsub_le_self : a - b ≤ a :=
  tsub_le_iff_left.mpr <| le_add_left le_rfl

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

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

Разделы

Аффилиация

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