add_sub_assoc

Mathlib.Data.Multiset.AddSub

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

English

If u ≤ t then s + t - u = s + (t - u).

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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