realize_sum — Mathlib

English

The realization of sum s f equals the sum of realizations: real(v, sum s f) = sum i∈s real(v, f(i)).

Русский

Реализация суммы s f равна сумме реализаций: real(v, sum s f) = ∑ i∈s real(v, f(i)).

LaTeX

$$$ \\operatorname{Term.realize} v (\\text{sum } s f) = \\sum_{i \\in s} \\operatorname{Term.realize} v (f i) $$$

Lean4

@[simp]
theorem realize_sum [AddCommMonoidWithOne M] {β : Type*} {s : Finset β} {f : β → presburger.Term α} :
    Term.realize v (sum s f) = ∑ i ∈ s, Term.realize v (f i) := by
  classical
  simp only [sum]
  conv => rhs; rw [← s.toList_toFinset, List.sum_toFinset _ s.nodup_toList]
  generalize s.toList = l
  induction l with simp [*]

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