Theorems · Theorem · sequences and series

Summable.tsum_subtype_le

∀ {κ : Type u_4} {γ : Type u_5} [inst : AddCommGroup γ] [inst_1 : PartialOrder γ] [IsOrderedAddMonoid γ]
  [inst_3 : UniformSpace γ] [IsUniformAddGroup γ] [OrderClosedTopology γ] [CompleteSpace γ] (f : κ → γ) (β : Set κ),
  (∀ (a : κ), 0 ≤ f a) → Summable f → ∑' (b : ↑β), f ↑b ≤ ∑' (a : κ), f a

Defined in

Mathlib.Topology.Algebra.InfiniteSum.Order

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommGroupPartialOrderIsOrderedAddMonoidUniformSpaceIsUniformAddGroupOrderClosedTopologyCompleteSpace