English
Let M be a commutative monoid, and let p be a predicate on M. If p is closed under multiplication (i.e., p(a) and p(b) imply p(a·b)) and s is a nonempty multiset in M for which p holds for every element, then p holds of the product of all elements of s.
Русский
Пусть M — коммутативная моноида; пусть p — свойство над M, и если p сохраняется при умножении (p(a) и p(b) ⇒ p(a·b)), а s — ненулевое мультимножество элементов M, для которого верно p для каждого элемента, то верно p произведения всех элементов s.
LaTeX
$$$\\forall M [\\mathsf{CommMonoid} M]\\, (p:M\\to \\mathsf{Prop})\\, (p\\_mul:\\forall a,b, p\\ a \\to p\\ b \\to p\\ (a b))\\, (s: \\mathsf{Multiset} M),\\; s \\neq \\emptyset \\;\\to\\; (\\forall a \\in s, p\\ a) \\;\\to\\; p\\left(s.prod\\right)$$$
Lean4
@[to_additive]
theorem prod_induction_nonempty (p : M → Prop) (p_mul : ∀ a b, p a → p b → p (a * b)) (hs : s ≠ ∅)
(p_s : ∀ a ∈ s, p a) : p s.prod := by
induction s using Multiset.induction_on with
| empty => simp at hs
| cons a s hsa =>
rw [prod_cons]
by_cases hs_empty : s = ∅
· simp [hs_empty, p_s a]
have hps : ∀ x, x ∈ s → p x := fun x hxs => p_s x (mem_cons_of_mem hxs)
exact p_mul a s.prod (p_s a (mem_cons_self a s)) (hsa hs_empty hps)
