English
Double bind with respect to two multisets m and n: (bind m) (λ a => (bind n) (λ b => f a b)) = (bind n) (λ b => (bind m) (λ a => f a b)).
Русский
Двойное связывание по двум мультимножества: (bind m) (λ a => (bind n) (λ b => f a b)) = (bind n) (λ b => (bind m) (λ a => f a b)).
LaTeX
$$$(\\mathrm{bind}\\, m)\\, (\\\\lambda a. (\\\\mathrm{bind}\\, n)\\\\, (\\\\lambda b. f\\\\,a\\\\,b)) = (\\\\mathrm{bind}\\, n)\\\\, (\\\\lambda b. (\\\\mathrm{bind}\\, m)\\\\, (\\\\lambda a. f\\\\,a\\\\,b))$$$
Lean4
theorem bind_bind (m : Multiset α) (n : Multiset β) {f : α → β → Multiset γ} :
((bind m) fun a => (bind n) fun b => f a b) = (bind n) fun b => (bind m) fun a => f a b :=
Multiset.induction_on m (by simp) (by simp +contextual)
