noncompactSpace — Mathlib

English

If X is a noncompact space and f: X → Y is a closed embedding, then Y is noncompact.

Русский

Если X некомпактно, и f: X → Y --- замкнутое вложение, то Y некомпактно.

LaTeX

$$$\text{NoncompactSpace}(X) \Rightarrow \text{NoncompactSpace}(Y)$ under a closed embedding $f$.$$

Lean4

protected theorem noncompactSpace [NoncompactSpace X] {f : X → Y} (hf : IsClosedEmbedding f) : NoncompactSpace Y :=
  noncompactSpace_of_neBot hf.tendsto_cocompact.neBot

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