isCompact_diagonal

Mathlib.Topology.Compactness.Compact

URI: https://scilib.ai/kg/mathlib#isCompact_diagonal

English

If X is compact, then the projection map Prod.snd: X × Y → Y is a closed map.

Русский

Если X компактно, отображение проекции Prod.snd: X × Y → Y является замкнутым отображением.

LaTeX

$$IsClosedMap(Prod.snd)$$

Lean4

theorem isCompact_diagonal [CompactSpace X] : IsCompact (diagonal X) :=
  @range_diag X ▸ isCompact_range (continuous_id.prodMk continuous_id)

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

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

Разделы

Аффилиация

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