Theorems · Theorem · sequences and series

rel_sup_add

∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {α : Type u_3} [inst_2 : CompleteLattice α]
  (m : α → M),
  m ⊥ = 0 →
    ∀ (R : M → M → Prop),
      (∀ (s : ℕ → α), R (m (⨆ i, s i)) (∑' (i : ℕ), m (s i))) → ∀ (s₁ s₂ : α), R (m (s₁ ⊔ s₂)) (m s₁ + m s₂)

If a function is countably sub-additive then it is binary sub-additive

Defined in

Mathlib.Topology.Algebra.InfiniteSum.NatInt

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommMonoidTopologicalSpaceCompleteLattice