map_id

Mathlib.Topology.Sets.Compacts

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.CompactOpens.map_id

English

The image of a compact-open set under the identity map is the set itself.

Русский

Образ компактно-открытого множества при единичном отображении совпадает с самим множеством.

LaTeX

$$K.map id continuous_id IsOpenMap.id = K$$

Lean4

@[simp]
theorem map_id (K : CompactOpens α) : K.map id continuous_id IsOpenMap.id = K :=
  CompactOpens.ext <| Set.image_id _

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

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

Разделы

Аффилиация

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