tsub_tsub_le — Mathlib

English

Let α be a preordered additive semigroup with subtraction. For any a,b ∈ α, we have b − (b − a) ≤ a.

Русский

Пусть α — упорядоченная полугруппа с операцией вычитания. Для любых a,b ∈ α выполнено: b − (b − a) ≤ a.

LaTeX

$$$b - (b - a) \le a$$$

Lean4

/-- See `tsub_tsub_cancel_of_le` for the equality. -/
theorem tsub_tsub_le : b - (b - a) ≤ a :=
  tsub_le_iff_right.mpr le_add_tsub

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