Mathlib Map

Theorems · Theorem · sequences and series

Summable.even_add_odd

∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M] {f : ℕ → M},
  (Summable fun k => f (2 * k)) → (Summable fun k => f (2 * k + 1)) → Summable f
Defined in
Mathlib.Topology.Algebra.InfiniteSum.NatInt
Cited by
1 results in Mathlib
Foundations
Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AddCommMonoidTopologicalSpaceContinuousAdd
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Summable.alternating · cited by 1Summable.alternatingTopologicalSpace · cited by 24529TopologicalSpaceAddCommMonoid · cited by 12281AddCommMonoidSummationFilter.unconditional · cited by 2068SummationFilter.unconditi…Summable · cited by 778SummableContinuousAdd · cited by 777ContinuousAddSummable.hasSum · cited by 184Summable.hasSumHasSum.summable · cited by 98HasSum.summableHasSum.even_add_odd · cited by 3HasSum.even_add_oddSummable.even_add_oddCITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.