isCompact

Mathlib.Topology.Compactness.SigmaCompact

URI: https://scilib.ai/kg/mathlib#CompactExhaustion.isCompact

English

For every n, the nth set K_n is compact.

Русский

Для каждого n множество K_n компактно.

LaTeX

$$$$\forall n \in \mathbb{N},\ IsCompact(K_n).$$$$

Lean4

protected theorem isCompact (n : ℕ) : IsCompact (K n) :=
  K.isCompact' n

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

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

Разделы

Аффилиация

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