map_id

Mathlib.Topology.Specialization

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

English

The map of the identity continuous map is the identity on the specialization order.

Русский

Картирование по тождественному отображению сохраняет идентичность на порядке специализации.

LaTeX

$$$\text{map}(\operatorname{ContinuousMap}.id\;\alpha) = \operatorname{OrderHom}.id$$$

Lean4

@[simp]
theorem map_id : map (ContinuousMap.id α) = OrderHom.id :=
  rfl

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

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

Разделы

Аффилиация

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