compactCovering — Mathlib

English

A canonical monotone covering by compact subsets of a space is defined by compactCovering.

Русский

Задан канонический монотонный покрывающий набор компактных подмножеств пространства — компактCovering.

LaTeX

$$compactCovering : ℕ → Set X; \\text{each } compactCovering(n) \\text{ is compact and } ⋃_n compactCovering(n) = univ (monotone).$$

Lean4

/-- A choice of compact covering for a `σ`-compact space, chosen to be monotone. -/
def compactCovering : ℕ → Set X :=
  Accumulate exists_compact_covering.choose

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