bind_none

Mathlib.Data.Part

URI: https://scilib.ai/kg/mathlib#Part.bind_none

English

Binding none with any f yields none.

Русский

Связывание пустого значения с функцией даёт пустое значение.

LaTeX

$$$\mathrm{none} \bind f = \mathrm{none}$$$

Lean4

@[simp]
theorem bind_none (f : α → Part β) : none.bind f = none :=
  eq_none_iff.2 fun a => by simp

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

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

Разделы

Аффилиация

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