map_some

Mathlib.Data.Part

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

English

Mapping with f preserves the Some value: map f (some a) = some (f a).

Русский

Преобразование через f сохраняет значение Some: map f (some a) = some (f a).

LaTeX

$$$ \forall {a} {f}, \mathrm{Part.map} f (\\mathrm{some } a) = \\mathrm{some }(f(a)) $$$

Lean4

@[simp]
theorem map_some (f : α → β) (a : α) : map f (some a) = some (f a) :=
  eq_some_iff.2 <| mem_map f <| mem_some _

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

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

Разделы

Аффилиация

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