theorem Multipliable.prod_le_tprod_set {ι : Type u_1} {α : Type u_2} [PartialOrder α] [CommGroup α] [IsOrderedMonoid α] [UniformSpace α] [IsUniformGroup α] [CompleteSpace α] [OrderClosedTopology α] {f : ι → α} {s : Finset ι} {t : Set ι} (hst : ↑s ⊆ t) (hfst : ∀ i ∉ s, i ∈ t → 1 ≤ f i) (hf : Multipliable f) : ∏ i ∈ s, f i ≤ ∏' (i : ↑t), f ↑i

theorem Summable.sum_le_tsum_set {ι : Type u_1} {α : Type u_2} [PartialOrder α] [AddCommGroup α] [IsOrderedAddMonoid α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] [OrderClosedTopology α] {f : ι → α} {s : Finset ι} {t : Set ι} (hst : ↑s ⊆ t) (hfst : ∀ i ∉ s, i ∈ t → 0 ≤ f i) (hf : Summable f) : ∑ i ∈ s, f i ≤ ∑' (i : ↑t), f ↑i