sub_sub_cancel

Mathlib.Data.ENat.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$$\forall a,b \in \mathbb{N}_\infty,\ a \ne \top \land b \le a \Rightarrow a - (a - b) = b.$$$$

Lean4

protected theorem sub_sub_cancel (h : a ≠ ⊤) (h2 : b ≤ a) : a - (a - b) = b :=
  (addLECancellable_of_ne_top <| ne_top_of_le_ne_top h tsub_le_self).tsub_tsub_cancel_of_le h2

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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