Theorems · Theorem · sequences and series

Summable.congr

∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f g : β → α}
  {L : SummationFilter β}, Summable f L → (∀ (b : β), f b = g b) → Summable g L

See Summable.congr_cofinite for a version allowing the functions to disagree on a finite set.

Defined in

Mathlib.Topology.Algebra.InfiniteSum.Basic

Cited by

20 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidTopologicalSpace