pure_bind

Mathlib.Order.Filter.Map

URI: https://scilib.ai/kg/mathlib#Filter.pure_bind

English

The bind of a pure element with m equals m a: bind (pure a) m = m a.

Русский

Связь чистого элемента через m даёт m a: bind (pure a) m = m a.

LaTeX

$$pure_bind (a : α) (m : α → Filter β) : bind (pure a) m = m a$$

Lean4

@[simp]
theorem pure_bind (a : α) (m : α → Filter β) : bind (pure a) m = m a := by simp only [bind, map_pure, join_pure]

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

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

Разделы

Аффилиация

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