add_tsub_cancel_iff_le — Mathlib

English

In a canonically ordered additive monoid with subtraction, a + (b − a) = b if and only if a ≤ b.

Русский

В канонически упорядоченном аддитивном полугруппе с вычитанием равенство a + (b − a) = b эквивалентно a ≤ b.

LaTeX

$$$$ a + (b - a) = b \iff a \le b $$$$

Lean4

theorem add_tsub_cancel_iff_le : a + (b - a) = b ↔ a ≤ b :=
  ⟨fun h => le_iff_exists_add.mpr ⟨b - a, h.symm⟩, add_tsub_cancel_of_le⟩

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