English
For a ≠ b, (f(a) + f(b))! times multinomial equals (f(a)+1) times multinomial with a incremented by 1.
Русский
Для a ≠ b, (f(a) + f(b))! × multinomial = (f(a) + 1) × multinomial с приращением f(a).
LaTeX
$$$ \\bigl(f(a) + f(b)\\bigr)\\! \\cdot \\operatorname{multinomial}({a,b}, f) = \\bigl(f(a) + 1\\bigr) \\cdot \\operatorname{multinomial}({a,b}, f[a \\mapsto f(a)+1]).$$$
Lean4
theorem succ_mul_binomial [DecidableEq α] (h : a ≠ b) :
(f a + f b).succ * multinomial { a, b } f = (f a).succ * multinomial { a, b } (Function.update f a (f a).succ) :=
by
rw [binomial_eq_choose h, binomial_eq_choose h, mul_comm (f a).succ, Function.update_self,
Function.update_of_ne h.symm]
rw [succ_mul_choose_eq (f a + f b) (f a), succ_add (f a) (f b)]
