subset_succ

Mathlib.Topology.Compactness.SigmaCompact

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

English

The union of all K_n equals the whole space X, i.e., the exhaustion covers X.

Русский

Союз всех K_n образует всё пространство X; исчерпывание охватывает X.

LaTeX

$$$$\bigcup_{n\in\mathbb{N}} K_n = X.$$$$

Lean4

theorem subset_succ (n : ℕ) : K n ⊆ K (n + 1) :=
  K.subset n.le_succ

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

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

Разделы

Аффилиация

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