English
For a family f: κ → γ that is pointwise bounded below by 1 and is Multipliable, the infinite product over a subset β ⊆ κ is bounded above by the full product over κ.
Русский
Для семейства f: κ → γ, где каждый f(a) ≥ 1 и существует множитель, имеющий свойство Multipliable, произведение по подмножеству β ⊆ κ не превосходит произведение по всему κ.
LaTeX
$$$\\forall f:\\ κ\\to γ,\\ β: Set\\ κ,\\ (\\forall a: κ, 1 \\le f(a))\\to \\text{Multipliable } f\\to \\left(\\prod'_{b\\in β} f(b) \\le \\prod'_{a\\in κ} f(a)\\right)$$$
Lean4
@[to_additive]
protected theorem tprod_subtype_le {κ γ : Type*} [CommGroup γ] [PartialOrder γ] [IsOrderedMonoid γ] [UniformSpace γ]
[IsUniformGroup γ] [OrderClosedTopology γ] [CompleteSpace γ] (f : κ → γ) (β : Set κ) (h : ∀ a : κ, 1 ≤ f a)
(hf : Multipliable f) : (∏' (b : β), f b) ≤ (∏' (a : κ), f a) :=
by
apply
Multipliable.tprod_le_tprod_of_inj _ (Subtype.coe_injective)
(by simp only [Subtype.range_coe_subtype, Set.setOf_mem_eq, h, implies_true])
(by simp only [le_refl, implies_true]) (by apply hf.subtype)
apply hf
