id

Mathlib.Topology.Maps.Basic

URI: https://scilib.ai/kg/mathlib#Topology.IsOpenEmbedding.id

English

The identity map on any space is an IsOpenEmbedding.

Русский

Идентичное отображение на любом пространстве является открытым вложением.

LaTeX

$$$ \text{IsOpenEmbedding}(@\mathrm{id}⁡ X) $$$

Lean4

protected theorem id : IsOpenEmbedding (@id X) :=
  ⟨.id, IsOpenMap.id.isOpen_range⟩

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

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

Разделы

Аффилиация

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