English
Let l be a multiset and f,g: ι → M with g(x) ≤ f(x) for all x in l; then sum of f−g over l equals sum f over l minus sum g over l.
Русский
Пусть l — мульсет, а f,g: ι → M так, что g(x) ≤ f(x) для всех x ∈ l; тогда сумма различий f(x)−g(x) по l равна разности сумм.
LaTeX
$$$\\displaystyle \\sum ( l.map (\\\\lambda x. f x - g x) ) = ( \\sum ( l.map f ) ) - ( \\sum ( l.map g ) )$$$
Lean4
theorem sum_map_tsub [AddCommMonoid M] [PartialOrder M] [ExistsAddOfLE M] [AddLeftMono M] [AddLeftReflectLE M] [Sub M]
[OrderedSub M] (l : Multiset ι) {f g : ι → M} (hfg : ∀ x ∈ l, g x ≤ f x) :
(l.map fun x ↦ f x - g x).sum = (l.map f).sum - (l.map g).sum :=
eq_tsub_of_add_eq <| by
rw [← sum_map_add]
congr 1
exact map_congr rfl fun x hx => tsub_add_cancel_of_le <| hfg _ hx
