add_sub_cancel

Mathlib.Data.Multiset.AddSub

URI: https://scilib.ai/kg/mathlib#Multiset.add_sub_cancel

English

t ≤ s → (s - t) + t = s.

Русский

Если t ≤ s, то (s - t) + t = s.

LaTeX

$$$t \le s \Rightarrow (s - t) + t = s$$$

Lean4

protected theorem add_sub_cancel (hts : t ≤ s) : s - t + t = s := by ext a;
  simp [Nat.sub_add_cancel <| count_le_of_le _ hts]

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

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

Разделы

Аффилиация

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