map_none

Mathlib.Data.Part

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

English

Mapping with any function f sends none to none: map f none = none.

Русский

Преобразование через функцию f отправляет none в none: map f none = none.

LaTeX

$$$ \forall {\alpha, \beta} (f : \alpha \to \beta), \mathrm{Part.map} f \mathrm{none} = \mathrm{none}$$$

Lean4

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

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

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

Разделы

Аффилиация

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