le_prod_nonempty_of_submultiplicative

English

If f : α → β is submultiplicative with f 1 = 1 and the conditions hold, then for any nonempty s, f(s.prod) ≤ (s.map f).prod.

Русский

Если f удовлетворяет субумножению и f(1)=1, и условия выполнены, то для любого непустого s имеет место f(s.prod) ≤ (s.map f).prod.

LaTeX

$$$ f : α \to β,\ h\_mul,\ h\_one,\ s : Multiset α,\ hs\_nonempty : s ≠ ∅ \Rightarrow f(s.prod) ≤ (s.map f).prod $$$

Lean4

@[to_additive le_sum_nonempty_of_subadditive]
theorem le_prod_nonempty_of_submultiplicative (f : α → β) (h_mul : ∀ a b, f (a * b) ≤ f a * f b) (s : Multiset α)
    (hs_nonempty : s ≠ ∅) : f s.prod ≤ (s.map f).prod :=
  le_prod_nonempty_of_submultiplicative_on_pred f (fun _ => True) (by simp [h_mul]) (by simp) s hs_nonempty (by simp)

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