IsSigmaCompact — Mathlib

English

A subset s ⊆ X is σ-compact if and only if there exists a sequence of subsets K_n ⊆ X such that every K_n is compact and s = ⋃_{n} K_n.

Русский

Подмножество s ⊆ X является σ-компактным тогда, когда существует последовательность множеств K_n ⊆ X, для которых каждый K_n компактно, и s равно объединению ⋃_{n} K_n.

LaTeX

$$$\exists K: \mathbb{N} \to Set X, (\forall n, IsCompact(K(n))) \land \bigcup_{n} K(n) = s$$$

Lean4

/-- A subset `s ⊆ X` is called **σ-compact** if it is the union of countably many compact sets. -/
def IsSigmaCompact (s : Set X) : Prop :=
  ∃ K : ℕ → Set X, (∀ n, IsCompact (K n)) ∧ ⋃ n, K n = s

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