Theorems · Theorem · sequences and series

rel_iSup_tprod

∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {α : Type u_3} {β : Type u_4} [Countable β]
  [inst_3 : CompleteLattice α] (m : α → M),
  m ⊥ = 1 →
    ∀ (R : M → M → Prop),
      (∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))) → ∀ (s : β → α), R (m (⨆ b, s b)) (∏' (b : β), m (s b))

If a function is countably sub-multiplicative then it is sub-multiplicative on countable types

Defined in

Mathlib.Topology.Algebra.InfiniteSum.NatInt

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommMonoidTopologicalSpaceCountableCompleteLattice