English
Same as previous, with the explicit nonempty predicate: if s ≠ ∅ and ∀ a ∈ s, p a, then f(s.prod) ≤ ∏_{a∈s} f(a).
Русский
То же самое: если s ≠ ∅ и для всех a ∈ s выполняется p a, то f(s.prod) ≤ ∏_{a∈s} 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_nonempty_of_subadditive_on_pred]
theorem le_prod_nonempty_of_submultiplicative_on_pred (f : α → β) (p : α → Prop)
(h_mul : ∀ a b, p a → p b → f (a * b) ≤ f a * f b) (hp_mul : ∀ a b, p a → p b → p (a * b)) (s : Multiset α)
(hs_nonempty : s ≠ ∅) (hs : ∀ a, a ∈ s → p a) : f s.prod ≤ (s.map f).prod :=
by
revert s
refine Multiset.induction ?_ ?_
· simp
rintro a s hs - hsa_prop
rw [prod_cons, map_cons, prod_cons]
by_cases hs_empty : s = ∅
· simp [hs_empty]
have hsa_restrict : ∀ x, x ∈ s → p x := fun x hx => hsa_prop x (mem_cons_of_mem hx)
have hp_sup : p s.prod := prod_induction_nonempty p hp_mul hs_empty hsa_restrict
have hp_a : p a := hsa_prop a (mem_cons_self a s)
exact (h_mul a _ hp_a hp_sup).trans (mul_le_mul_left' (hs hs_empty hsa_restrict) _)
