English
Let s be a finite set, f: α → β, and P a property on β closed under multiplication. If P(1) holds, and P(f(a)) holds for every a ∈ s, then P(s.noncommProd f comm) holds.
Русский
Пусть s — конечное множество, f: α → β, и P — свойство на β, сохраняющее умножение. Пусть P(1) выполняется, и P(f(a)) выполняется для каждого a ∈ s; тогда P(некоммопрод) выполняется.
LaTeX
$$$ (s : \mathrm{Finset} \; \alpha) \; (f : \alpha \to \beta) \; (comm) \; (p : \beta \to \mathrm{Prop}) \\; (hom : \forall a b, p a \to p b \to p (a \cdot b)) \\; (unit : p 1) \; (base : \forall x \in s, p (f x)) \\; \Rightarrow p (s.noncommProd f comm)$$$
Lean4
@[to_additive]
theorem noncommProd_induction (s : Finset α) (f : α → β) (comm) (p : β → Prop) (hom : ∀ a b, p a → p b → p (a * b))
(unit : p 1) (base : ∀ x ∈ s, p (f x)) : p (s.noncommProd f comm) :=
by
refine Multiset.noncommProd_induction _ _ _ hom unit fun b hb ↦ ?_
obtain (⟨a, ha : a ∈ s, rfl : f a = b⟩) := by simpa using hb
exact base a ha
