isCompact_accumulate

Mathlib.Topology.Compactness.Compact

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

← MathLib Explorer

English

If each K n is compact, then Accumulate(K, n) is compact.

Русский

Если каждое K_n компактно, то аккумулятивное объединение Accumulate(K,n) компактно.

LaTeX

$$$\\text{IsCompact } (Accumulate\\, K\\, n)$$$

Lean4

theorem isCompact_accumulate {K : ℕ → Set X} (hK : ∀ n, IsCompact (K n)) (n : ℕ) : IsCompact (Accumulate K n) :=
  (finite_le_nat n).isCompact_biUnion fun k _ => hK k

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

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

Разделы

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

Аффилиация

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