bind_map_comm — Mathlib

English

A relation between map and bind: (bind m) (λ a => n.map (λ b => f a b)) = (bind m) (λ a => map f (n a)).

Русский

Связь между map и bind: (bind m) (λ a ⇒ n.map (λ b ⇒ f a b)) = (bind m) (λ a ⇒ map f (n a)).

LaTeX

$$$(\\mathrm{bind}\\, m)\\\\, (\\\\lambda a. n.\\\\map\\\\, (\\\\lambda b. f a b)) = (\\\\mathrm{bind}\\, m)\\\\, (\\\\lambda a. \\\\mathrm{map}\\\\, f \\\\,(n \\\\ a))$$$

Lean4

theorem bind_map_comm (m : Multiset α) (n : Multiset β) {f : α → β → γ} :
    ((bind m) fun a => n.map fun b => f a b) = (bind n) fun b => m.map fun a => f a b :=
  Multiset.induction_on m (by simp) (by simp +contextual)

Похожие утверждения