map_id

Mathlib.Topology.Compactification.OnePoint.Basic

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

English

The construction OnePoint.map preserves the identity map: applying OnePoint.map to the identity on X yields the identity on OnePoint X.

Русский

Конструкция OnePoint.map сохраняет тождественную карту: OnePoint.map(identity) = identity на OnePoint X.

LaTeX

$$$\\mathrm{OnePoint.map}(\\mathrm{id}_X) = \\mathrm{id}_{\\mathrm{OnePoint} X}.$$$

Lean4

@[simp]
theorem map_id : OnePoint.map (id : X → X) = id :=
  Option.map_id

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

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

Разделы

Аффилиация

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