isClosed — Mathlib

English

In a T2 space, a compact exhaustion K has closed stages: each K n is closed.

Русский

В T2-пространстве последовательность компактного исчерпания K имеет замкнутые ступени: каждый K n замкнут.

LaTeX

$$$[T2Space X] (K: CompactExhaustion X) (n:\\mathbb{N})\\Rightarrow IsClosed (K(n)).$$$

Lean4

theorem isClosed [T2Space X] (K : CompactExhaustion X) (n : ℕ) : IsClosed (K n) :=
  (K.isCompact n).isClosed

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