bind_cons — Mathlib

English

Bind with a cons inside: (s.bind (λ a => Multiset.cons (f a) (g a))) = map f s + s.bind g.

Русский

Связывание внутри с конструктором: (s.bind (λ a, Multiset.cons (f a) (g a))) = map f s + s.bind g.

LaTeX

$$$\\bigl(s.bind (\\lambda a. \\mathrm{Multiset.cons}(f a)(g a))\\bigr) = \\mathrm{Multiset.map} f\\, s + s.bind g$$$

Lean4

@[simp]
theorem bind_cons (f : α → β) (g : α → Multiset β) : (s.bind fun a => f a ::ₘ g a) = map f s + s.bind g :=
  Multiset.induction_on s (by simp) (by simp +contextual [add_comm, add_left_comm, add_assoc])

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