sum_add_distrib — Mathlib

English

The sum distributes over addition pointwise: sum (f + g) = sum f + sum g.

Русский

Сумма распространяется по сложению поэлементно: сумма (f + g) = сумма f + сумма g.

LaTeX

$$$\\sum (f + g) = \\sum f + \\sum g$$$

Lean4

@[simp]
theorem sum_add_distrib {ι} (f g : ι → Cardinal) : sum (f + g) = sum f + sum g :=
  by
  have := mk_congr (Equiv.sigmaSumDistrib (Quotient.out ∘ f) (Quotient.out ∘ g))
  simp only [comp_apply, mk_sigma, mk_sum, mk_out, lift_id] at this
  exact this

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