sub_add_eq_sub_sub

Mathlib.Data.Multiset.AddSub

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

English

For all s,t,u multisets, s − (t + u) = s − t − u.

Русский

Для любых мультимножества s,t,u верно: s − (t + u) = s − t − u.

LaTeX

$$$$ s - (t + u) = s - t - u $$$$

Lean4

protected theorem sub_add_eq_sub_sub : s - (t + u) = s - t - u := by ext; simp [Nat.sub_add_eq]

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

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

Разделы

Аффилиация

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