English
For a ≠ b, updating f by increasing at a and b yields a relation: multinomial {a,b} (f with a+1, b+1) equals sum of multinomials with a+1 and with b+1.
Русский
Для a ≠ b обновление f на a и b приводит к равенству: multinomial{a,b}(f с a+1 и b+1) = multinomial{a,b}(f с a+1) + multinomial{a,b}(f с b+1).
LaTeX
$$$ \\operatorname{multinomial}({a,b},\\text{update}(f,a, f(a)\\!\\!\\!\\+1), \\text{update}(f,b, f(b)\\!\\!\\+1)) = \\operatorname{multinomial}({a,b},\\text{update}(f,a, f(a)\\+1)) + \\operatorname{multinomial}({a,b},\\text{update}(f,b, f(b)\\+1)).$$$
Lean4
theorem binomial_succ_succ [DecidableEq α] (h : a ≠ b) :
multinomial { a, b } (Function.update (Function.update f a (f a).succ) b (f b).succ) =
multinomial { a, b } (Function.update f a (f a).succ) + multinomial { a, b } (Function.update f b (f b).succ) :=
by
simp only [binomial_eq_choose, Function.update_apply, h, Ne, ite_true, ite_false, not_false_eq_true]
rw [if_neg h.symm]
rw [add_succ, choose_succ_succ, succ_add_eq_add_succ]
ring
