Theorems · Theorem · sequences and series

Multipliable.tprod_subtype_le

∀ {κ : Type u_4} {γ : Type u_5} [inst : CommGroup γ] [inst_1 : PartialOrder γ] [IsOrderedMonoid γ]
  [inst_3 : UniformSpace γ] [IsUniformGroup γ] [OrderClosedTopology γ] [CompleteSpace γ] (f : κ → γ) (β : Set κ),
  (∀ (a : κ), 1 ≤ f a) → Multipliable f → ∏' (b : ↑β), f ↑b ≤ ∏' (a : κ), f a

Defined in

Mathlib.Topology.Algebra.InfiniteSum.Order

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommGroupPartialOrderIsOrderedMonoidUniformSpaceIsUniformGroupOrderClosedTopologyCompleteSpace