sum_add_distrib'

Mathlib.SetTheory.Cardinal.Order

URI: https://scilib.ai/kg/mathlib#Cardinal.sum_add_distrib'

English

The version with a prime marker: sum (f i + g i) = sum f + sum g.

Русский

Версия с пометкой примы: сумма (f i + g i) = сумма f + сумма g.

LaTeX

$$$\\operatorname{sum} (\\lambda i. f(i) + g(i)) = \\operatorname{sum} f + \\operatorname{sum} g$$$

Lean4

@[simp]
theorem sum_add_distrib' {ι} (f g : ι → Cardinal) : (Cardinal.sum fun i => f i + g i) = sum f + sum g :=
  sum_add_distrib f g

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

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

Разделы

Аффилиация

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