coe_id

Mathlib.Topology.Hom.Open

URI: https://scilib.ai/kg/mathlib#ContinuousOpenMap.coe_id

English

The functorial value of the identity open map equals the identity map.

Русский

Значение функции от тождества открытого отображения равно тождественной функции.

LaTeX

$$$\operatorname{coe}(\text{ContinuousOpenMap.id } α) = \mathrm{id}.$$$

Lean4

@[simp, norm_cast]
theorem coe_id : ⇑(ContinuousOpenMap.id α) = id :=
  rfl

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

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

Разделы

Аффилиация

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