single_le_prod_of_canonicallyOrdered

English

If s ⊆ t, then ∏_{x ∈ s} f(x) ≤ ∏_{x ∈ t} f(x).

Русский

Если s ⊆ t, то произведение значений f на s не превосходит произведение на t.

LaTeX

$$$s \\subseteq t \\Rightarrow \\prod_{x \\in s} f(x) \\le \\prod_{x \\in t} f(x)$$$

Lean4

/-- In a canonically-ordered monoid, a product bounds each of its terms.

See also `Finset.single_le_prod'`. -/
@[to_additive /-- In a canonically-ordered additive monoid, a sum bounds each of its terms.

    See also `Finset.single_le_sum`. -/
    ]
theorem single_le_prod_of_canonicallyOrdered {i : ι} (hi : i ∈ s) : f i ≤ ∏ j ∈ s, f j :=
  have := CanonicallyOrderedMul.toIsOrderedMonoid (α := M)
  single_le_prod' (fun _ _ ↦ one_le _) hi

Похожие утверждения