map_eq_id

Mathlib.Data.Option.Basic

URI: https://scilib.ai/kg/mathlib#Option.map_eq_id

English

The map f equals the identity map iff f is the identity.

Русский

map f равно identity тогда и только тогда, когда f = id.

LaTeX

$$$$ \operatorname{map} f = \mathrm{id} \iff f = \mathrm{id}. $$$$

Lean4

@[simp]
theorem map_eq_id {f : α → α} : Option.map f = id ↔ f = id :=
  map_injective'.eq_iff' map_id

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

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

Разделы

Аффилиация

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