Theorems · Theorem · sequences and series

rel_iSup_prod

∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {α : Type u_3} {γ : Type u_5}
  [inst_2 : CompleteLattice α] (m : α → M),
  m ⊥ = 1 →
    ∀ (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-multiplicative then it is sub-multiplicative on finite sets

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

CommMonoidTopologicalSpaceCompleteLattice