isCompact_insert_range — Mathlib

English

If f tends to x along atTop, then insert x (range f) is compact.

Русский

Если f сходится к x по atTop, то x вместе с range f компактны.

LaTeX

$$$\operatorname{Tendsto}(f, \operatorname{atTop}, \mathcal{N}(x)) \Rightarrow \operatorname{IsCompact}(\operatorname{insert}(x, \operatorname{range}(f)))$$$

Lean4

theorem isCompact_insert_range {f : ℕ → X} {x} (hf : Tendsto f atTop (𝓝 x)) : IsCompact (insert x (range f)) :=
  Filter.Tendsto.isCompact_insert_range_of_cofinite <| Nat.cofinite_eq_atTop.symm ▸ hf

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