English
If f: X → Y tends to y along the coLindelof filter and f is continuous, then the set insert y (range f) is Lindelöf.
Русский
Если f имеет предел y по ко-Линдельфовскому фильтру и непрерывна, то множество insert y (range f) Линдельоф.
LaTeX
$$$\forall f:\ X\to Y, \ y,\; (\mathrm{Tendsto}\ f\ (\mathrm{coLindelof}\ X)\ (\mathcal{N}(y)))\land Continuous(f) \Rightarrow IsLindelof(\mathrm{insert}\ y\ (\mathrm{range}\ f))$$$
Lean4
theorem isLindelof_insert_range_of_coLindelof {f : X → Y} {y} (hf : Tendsto f (coLindelof X) (𝓝 y))
(hfc : Continuous f) : IsLindelof (insert y (range f)) :=
by
intro l hne _ hle
by_cases hy : ClusterPt y l
· exact ⟨y, Or.inl rfl, hy⟩
simp only [clusterPt_iff_nonempty, not_forall, ← not_disjoint_iff_nonempty_inter, not_not] at hy
rcases hy with ⟨s, hsy, t, htl, hd⟩
rcases mem_coLindelof.1 (hf hsy) with ⟨K, hKc, hKs⟩
have : f '' K ∈ l := by
filter_upwards [htl, le_principal_iff.1 hle] with y hyt hyf
rcases hyf with (rfl | ⟨x, rfl⟩)
exacts [(hd.le_bot ⟨mem_of_mem_nhds hsy, hyt⟩).elim,
mem_image_of_mem _ (not_not.1 fun hxK => hd.le_bot ⟨hKs hxK, hyt⟩)]
rcases hKc.image hfc (le_principal_iff.2 this) with ⟨y, hy, hyl⟩
exact ⟨y, Or.inr <| image_subset_range _ _ hy, hyl⟩
