Theorems · Theorem · sequences and series

rel_iSup_sum

∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {α : Type u_3} {γ : Type u_5}
  [inst_2 : CompleteLattice α] (m : α → M),
  m ⊥ = 0 →
    ∀ (R : M → M → Prop),
      (∀ (s : ℕ → α), R (m (⨆ i, s i)) (∑' (i : ℕ), m (s i))) →
        ∀ (s : γ → α) (t : Finset γ), R (m (⨆ d ∈ t, s d)) (∑ d ∈ t, m (s d))

If a function is countably sub-additive then it is sub-additive on finite sets

Defined in

Mathlib.Topology.Algebra.InfiniteSum.NatInt

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommMonoidTopologicalSpaceCompleteLattice