nonLindelofSpace — Mathlib

English

If X is non-Lindelöf and f:X→Y is a closed embedding, then Y is non-Lindelöf.

Русский

Если X не Линдельфово и существует замкнутое вложение f: X → Y, то Y тоже не Линдельфово.

LaTeX

$$$[\\text{NonLindelofSpace}(X)]\\; \\text{and } f:X\\to Y \\text{ closed embedding } \\Rightarrow \\text{NonLindelofSpace}(Y).$$$

Lean4

protected theorem nonLindelofSpace [NonLindelofSpace X] {f : X → Y} (hf : IsClosedEmbedding f) : NonLindelofSpace Y :=
  nonLindelofSpace_of_neBot hf.tendsto_coLindelof.neBot

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