instCompactSpaceSubtypeMem

Mathlib.Topology.Sets.Compacts

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Compacts.instCompactSpaceSubtypeMem

English

If K is a compact subset of α, then the subspace of α restricted to K is a compact space.

Русский

Если K компактно как подмножество α, то подпространство K внутри α является компактным пространством.

LaTeX

$$$CompactSpace(\Subtype\{x : α \mid x \in K\})$$$

Lean4

instance (K : Compacts α) : CompactSpace K :=
  isCompact_iff_compactSpace.1 K.isCompact

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

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

Разделы

Аффилиация

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