bind_map

Mathlib.Data.Multiset.Bind

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

← MathLib Explorer

English

Same as Map-Bind above: map f (bind m n) = bind m (λ a, map f (n a)).

Русский

То же самое: map f (bind m n) = bind m (λ a, map f (n a)).

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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