English
Let f be a submultiplicative map from M to N, p a predicate on M, and g_i a finite family in M with p(g_i). Then f(product over i∈s of g_i) ≤ product over i∈s f(g_i).
Русский
Пусть f субумножима на M→N, p на M, а g_i — конечная семья в M с условием p(g_i). Тогда f(произведение) ≤ произведение f(g_i).
LaTeX
$$$f (\\prod_{i\\in s} g_i) \\le \\prod_{i\\in s} f (g_i)$$$
Lean4
/-- Let `{x | p x}` be a subsemigroup of a commutative monoid `M`. Let `f : M → N` be a map
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 nonempty finite family of elements of `M` such that `∀ i ∈ s, p (g i)`. Then
`f (∏ x ∈ s, g x) ≤ ∏ x ∈ s, f (g x)`. -/
@[to_additive le_sum_nonempty_of_subadditive_on_pred]
theorem le_prod_nonempty_of_submultiplicative_on_pred [IsOrderedMonoid N] (f : M → N) (p : M → Prop)
(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_nonempty : s.Nonempty) (hs : ∀ i ∈ s, p (g i)) : f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i) :=
by
refine le_trans (Multiset.le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul _ ?_ ?_) ?_
· simp [hs_nonempty.ne_empty]
· exact Multiset.forall_mem_map_iff.mpr hs
simp
