le_prod_of_submultiplicative — Mathlib

English

If f is submultiplicative, then for any finite nonempty s, f of the product is at most the product of f(g_i).

Русский

Если f субумножима, то для любого непустого конечного s верно: f(произведение) ≤ произведение f(g_i).

LaTeX

$$$f(\\prod i∈s, g_i) ≤ \\prod i∈s f(g_i)$$$

Lean4

/-- If `f : M → N` is a submultiplicative function, `f (x * y) ≤ f x * f y`, `f 1 = 1`, and `g i`,
`i ∈ s`, is a finite family of elements of `M`, then `f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)`. -/
@[to_additive le_sum_of_subadditive]
theorem le_prod_of_submultiplicative [IsOrderedMonoid N] (f : M → N) (h_one : f 1 = 1)
    (h_mul : ∀ x y, f (x * y) ≤ f x * f y) (s : Finset ι) (g : ι → M) : f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i) :=
  le_trans (Multiset.le_prod_of_submultiplicative f h_one h_mul _) (by simp)

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