English
Let f: X → Y be a closed embedding between topological spaces. Then f is proper with respect to Lindelöfness: for every Lindelöf subset L ⊆ Y, the preimage f^{-1}(L) is Lindelöf in X. Equivalently, f carries the coLindelöf filter on X into the coLindelöf filter on Y (i.e. Tendsto f(coLindelof X) (coLindelof Y)).
Русский
Пусть f: X → Y — замкнутое вложение между топологическими пространствами. Тогда f является Proper относительно Линдельфовости: для любой Линдельфовой подмножости L ⊆ Y её прообраз f^{-1}(L) является Линдельфовским в X. Эквивалентно, отображение f отправляет фильтр coLindelof(X) в фильтр coLindelof(Y).
LaTeX
$$$\\text{If } f:X\\to Y \\text{ is a closed embedding, then for every } L\\subseteq Y,\\; \\operatorname{Lindelöf}(L) \\Rightarrow \\operatorname{Lindelöf}(f^{-1}(L)).$$$
Lean4
/-- A closed embedding is proper, i.e., inverse images of Lindelöf sets are contained in Lindelöf.
Moreover, the preimage of a Lindelöf set is Lindelöf, see
`Topology.IsClosedEmbedding.isLindelof_preimage`. -/
theorem tendsto_coLindelof {f : X → Y} (hf : IsClosedEmbedding f) :
Tendsto f (Filter.coLindelof X) (Filter.coLindelof Y) :=
hasBasis_coLindelof.tendsto_right_iff.mpr fun _K hK => (hf.isLindelof_preimage hK).compl_mem_coLindelof
