LindelofSpace — Mathlib

English

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

Русский

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

LaTeX

$$$[\\text{LindelöfSpace}(Y)] \\Rightarrow (\\, \\text{IsClosedEmbedding}(f) \\Rightarrow \\text{LindelöfSpace}(X)\\,).$$$

Lean4

protected theorem LindelofSpace [h : LindelofSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) : LindelofSpace X :=
  ⟨by rw [hf.isInducing.isLindelof_iff, image_univ]; exact hf.isClosed_range.isLindelof⟩

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