le_prod_of_submultiplicative — Mathlib

English

If f : α → β is submultiplicative on a predicate p and s is nonempty with p a for all a ∈ s, then f(s.prod) ≤ ∏_{a∈s} f(a).

Русский

Если f удовлетворяет субумножению на предикат p и s непусто с p(a) для всех a ∈ s, то f(s.prod) ≤ ∏ f(a).

LaTeX

$$$ f : α \to β,\ p,\ h\_mul,\ hp\_mul,\ s : Multiset α,\ hs\_nonempty : s ≠ ∅,\ hs : ∀ a, a ∈ s → p a \Rightarrow f(s.prod) ≤ (s.map f).prod $$$

Lean4

@[to_additive le_sum_of_subadditive]
theorem le_prod_of_submultiplicative (f : α → β) (h_one : f 1 = 1) (h_mul : ∀ a b, f (a * b) ≤ f a * f b)
    (s : Multiset α) : f s.prod ≤ (s.map f).prod :=
  le_prod_of_submultiplicative_on_pred f (fun _ => True) h_one trivial (fun x y _ _ => h_mul x y) (by simp) s (by simp)

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