id

Mathlib.Topology.Maps.OpenQuotient

URI: https://scilib.ai/kg/mathlib#IsOpenQuotientMap.id

English

The identity map id: X → X is an open quotient map.

Русский

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

LaTeX

$$$\mathrm{IsOpenQuotientMap}(\mathrm{id})$$$

Lean4

protected theorem id : IsOpenQuotientMap (id : X → X) :=
  ⟨surjective_id, continuous_id, .id⟩

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

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

Разделы

Аффилиация

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