cons_bind

Mathlib.Data.Multiset.Bind

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

English

Distributivity of bind over cons: (a :: s).bind f = f a + s.bind f.

Русский

Дистрибутивность связывания над конструктором: (a :: s).bind f = f a + s.bind f.

LaTeX

$$$ (a :: s).bind f = f\\,a + s.bind f$$$

Lean4

@[simp]
theorem cons_bind : (a ::ₘ s).bind f = f a + s.bind f := by simp [bind]

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

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

Разделы

Аффилиация

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