isCompact_range

Mathlib.Topology.Compactness.Compact

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

← MathLib Explorer

English

If X is compact, then the diagonal in X × X is compact.

Русский

Если X компактно, диагональ в X × X компактна.

LaTeX

$$IsCompact( diagonal(X) )$$

Lean4

theorem isCompact_range [CompactSpace X] {f : X → Y} (hf : Continuous f) : IsCompact (range f) := by rw [← image_univ];
  exact isCompact_univ.image hf

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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