map_out

Mathlib.Data.Erased

URI: https://scilib.ai/kg/mathlib#Erased.map_out

English

Mapping a function f through Erased α yields that the output equals f applied to the erased value: (a.map f).out = f(a.out).

Русский

Построение через Erased α сохраняет результат: (a.map f).out = f(a.out).

LaTeX

$$$(\\mathrm{Erased}.map\\ f\\ a).out = f\\ (a.out)$$$

Lean4

@[simp]
theorem map_out {α β} {f : α → β} (a : Erased α) : (a.map f).out = f a.out := by simp [map]

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

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

Разделы

Аффилиация

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