English
Let s be a Lindelöf subset of X and f: X → Y be a function that is continuous on s. Then the image f[s] is a Lindelöf subset of Y.
Русский
Пусть s — множество Линдельёфа в X, и f: X → Y непрерывна на s. Тогда образ f[s] — множество Линдельёфа в Y.
LaTeX
$$$\text{If } s \subset X \text{ is Lindelöf and } f: X \to Y \text{ is continuous on } s, \text{ then } f[S] \text{ is Lindelöf in } Y.$$$
Lean4
/-- A continuous image of a Lindelöf set is a Lindelöf set. -/
theorem image_of_continuousOn {f : X → Y} (hs : IsLindelof s) (hf : ContinuousOn f s) : IsLindelof (f '' s) :=
by
intro l lne _ ls
have : NeBot (l.comap f ⊓ 𝓟 s) := comap_inf_principal_neBot_of_image_mem lne (le_principal_iff.1 ls)
obtain ⟨x, hxs, hx⟩ : ∃ x ∈ s, ClusterPt x (l.comap f ⊓ 𝓟 s) := @hs _ this _ inf_le_right
haveI := hx.neBot
use f x, mem_image_of_mem f hxs
have : Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l) :=
by
convert (hf x hxs).inf (@tendsto_comap _ _ f l) using 1
rw [nhdsWithin]
ac_rfl
exact this.neBot
