English
If f is submultiplicative and nondecreasing with 1 mapped to 1, then the bound holds for any nonempty Finset s: f(prod g_i) ≤ prod f(g_i).
Русский
Если f субумножима и монотонна с f(1)=1, то неравенство справедливо для любого непустого Finset: 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` and `g i`, `i ∈ s`, is a
nonempty finite family of elements of `M`, then `f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)`. -/
@[to_additive le_sum_nonempty_of_subadditive]
theorem le_prod_nonempty_of_submultiplicative [IsOrderedMonoid N] (f : M → N) (h_mul : ∀ x y, f (x * y) ≤ f x * f y)
{s : Finset ι} (hs : s.Nonempty) (g : ι → M) : f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i) :=
le_prod_nonempty_of_submultiplicative_on_pred f (fun _ ↦ True) (fun x y _ _ ↦ h_mul x y) (fun _ _ _ _ ↦ trivial) g s
hs fun _ _ ↦ trivial
