sub_sub_cancel

Mathlib.Data.ENNReal.Operations

URI: https://scilib.ai/kg/mathlib#ENNReal.sub_sub_cancel

English

If a ≠ ∞ and b ≤ a, then a − (a − b) = b.

Русский

Если a ≠ ∞ и b ≤ a, то a − (a − b) = b.

LaTeX

$$$ (a \neq \infty) \land (b \le a) \Rightarrow a - (a - b) = b $$$

Lean4

theorem sub_sub_cancel (h : a ≠ ∞) (h2 : b ≤ a) : a - (a - b) = b :=
  (cancel_of_ne <| sub_ne_top h).tsub_tsub_cancel_of_le h2

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

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

Разделы

Аффилиация

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