sum_Ico_add_eq_sum_Ico_add_one — Mathlib

English

Let a ≤ b in a linear order with LocallyFiniteOrder, and f: α → M in an additive monoid with one. Then ∑_{x ∈ Ico(a,b)} f(x) + f(b) = ∑_{x ∈ Ico(a,b+1)} f(x).

Русский

Пусть a ≤ b в линейном порядке с локально-конечным порядком и f: α → M в аддитивном монаде с единицей. Тогда сумма по Ico(a,b) плюс f(b) равна сумме по Ico(a,b+1).

LaTeX

$$$ \sum_{x \in \mathrm{Ico}(a,b)} f(x) + f(b) = \sum_{x \in \mathrm{Ico}(a,(b+1))} f(x) $$$

Lean4

theorem sum_Ico_add_eq_sum_Ico_add_one {M : Type*} [AddCommMonoid M] (hab : a ≤ b) (f : α → M) :
    ∑ x ∈ Ico a b, f x + f b = ∑ x ∈ Ico a (b + 1), f x := by
  rw [← Finset.insert_Ico_right_eq_Ico_add_one hab, sum_insert right_notMem_Ico, add_comm]

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