isCompact_insert_range_of_cofinite

English

If f tends to x along cofinite, 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_cofinite {f : ι → X} {x} (hf : Tendsto f cofinite (𝓝 x)) :
    IsCompact (insert x (range f)) := by
  letI : TopologicalSpace ι := ⊥; haveI h : DiscreteTopology ι := ⟨rfl⟩
  rw [← cocompact_eq_cofinite ι] at hf
  exact hf.isCompact_insert_range_of_cocompact continuous_of_discreteTopology

Похожие утверждения