English
Let f be a submultiplicative map with f(1)=1; for a finite nonempty s, and g: s→M with p(g_i) for all i, then f of the s-product is bounded by the s-product of f(g_i).
Русский
Пусть f субумножима и f(1)=1; для конечного непустого s и g: s→M с p(g_i) выполняется требование.
LaTeX
$$$f(\\prod i∈s, g_i) ≤ \\prod i∈s f(g_i)$$$
Lean4
/-- Let `{x | p x}` be a subsemigroup of a commutative monoid `M`. Let `f : M → N` be a map
such that `f 1 = 1` and `f` is submultiplicative on `{x | p x}`, i.e.,
`p x → p y → f (x * y) ≤ f x * f y`. Let `g i`, `i ∈ s`, be a finite family of elements of `M` such
that `∀ i ∈ s, p (g i)`. Then `f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)`. -/
@[to_additive le_sum_of_subadditive_on_pred]
theorem le_prod_of_submultiplicative_on_pred [IsOrderedMonoid N] (f : M → N) (p : M → Prop) (h_one : f 1 = 1)
(h_mul : ∀ x y, p x → p y → f (x * y) ≤ f x * f y) (hp_mul : ∀ x y, p x → p y → p (x * y)) (g : ι → M)
{s : Finset ι} (hs : ∀ i ∈ s, p (g i)) : f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i) :=
by
rcases eq_empty_or_nonempty s with (rfl | hs_nonempty)
· simp [h_one]
· exact le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul g s hs_nonempty hs
