map_id

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#WithBot.map_id

English

Applying the identity map inside WithBot yields the identity: map id = id.

Русский

Применение тождевого отображения внутри WithBot даёт тождественное отображение: map id = id.

LaTeX

$$$\mathrm{WithBot.map}(\mathrm{id}) = \mathrm{id}$$$

Lean4

theorem map_id : map (id : α → α) = id :=
  Option.map_id

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

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

Разделы

Аффилиация

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