bind_singleton

Mathlib.Data.Multiset.Bind

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

← MathLib Explorer

English

Binding over a singleton returns the singleton image: bind {a} f = map to a of f a.

Русский

Связывание над единичным множеством даёт образ: bind {a} f = map f a.

LaTeX

$$$(s.bind \\lambda x. \\{f x\\}) = map f s$$$

Lean4

@[simp]
theorem bind_singleton (f : α → β) : (s.bind fun x => ({f x} : Multiset β)) = map f s :=
  Multiset.induction_on s (by rw [zero_bind, map_zero]) (by simp [singleton_add])

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

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

Разделы

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

Аффилиация

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