English
For a continuous map f, the comap of the coLindelöf filter on Y is less or equal to the coLindelöf filter on X.
Русский
Для непрерывного отображения f, обратный образ фильтра coLindelof на Y включается в фильтр coLindelof на X.
LaTeX
$$${f:X→Y}\ (hf: Continuous f) : (Filter.coLindelof Y).comap f ≤ Filter.coLindelof X$$$
Lean4
/-- The comap of the coLindelöf filter on `Y` by a continuous function `f : X → Y` is less than or
equal to the coLindelöf filter on `X`.
This is a reformulation of the fact that images of Lindelöf sets are Lindelöf. -/
theorem comap_coLindelof_le {f : X → Y} (hf : Continuous f) : (Filter.coLindelof Y).comap f ≤ Filter.coLindelof X :=
by
rw [(hasBasis_coLindelof.comap f).le_basis_iff hasBasis_coLindelof]
intro t ht
refine ⟨f '' t, ht.image hf, ?_⟩
simpa using t.subset_preimage_image f
