bind_assoc

Mathlib.Data.Multiset.Bind

URI: https://scilib.ai/kg/mathlib#Multiset.bind_assoc

← MathLib Explorer

English

Associativity of bind: (s.bind f).bind g = s.bind (λ a, (f a).bind g).

Русский

Ассоциативность связывания: (s.bind f).bind g = s.bind (λ a, (f a).bind g).

LaTeX

$$$(s.bind f).bind g = s.bind (\\lambda a. (f\\,a).bind g)$$$

Lean4

theorem bind_assoc {s : Multiset α} {f : α → Multiset β} {g : β → Multiset γ} :
    (s.bind f).bind g = s.bind fun a => (f a).bind g :=
  Multiset.induction_on s (by simp) (by simp +contextual)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru