English
If f tends to x through the cofinite filter, then insert x (range f) is compact.
Русский
Если f сходится к x по кофинитному фильтру, то множество x вместе с range f компактно.
LaTeX
$$$\operatorname{Tendsto}(f, \operatorname{cofinite}, \mathcal{N}(x)) \Rightarrow \operatorname{IsCompact}(\operatorname{insert}(x, \operatorname{range}(f)))$$$
Lean4
theorem isCompact_insert_range_of_cocompact {f : X → Y} {y} (hf : Tendsto f (cocompact X) (𝓝 y)) (hfc : Continuous f) :
IsCompact (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_cocompact.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⟩
