iUnion_eq

Mathlib.Topology.Compactness.SigmaCompact

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

English

The union over n of the nth member of the exhaustion equals the space; a restatement of Union property.

Русский

Объединение по всем n членов исчерпывания равно пространству; повторение свойства объединения.

LaTeX

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

Lean4

theorem iUnion_eq : ⋃ n, K n = univ :=
  K.iUnion_eq'

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

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

Разделы

Аффилиация

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