sub_add_cancel

Mathlib.Data.Multiset.AddSub

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

English

Let s and t be multisets with t contained in s. Then s − t + t = s.

Русский

Пусть s и t — мультимножества, при этом t является подмультимножество s. Тогда s − t + t = s.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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