tendsto_nhds_infty' — Mathlib

English

Characterization: f ≤ 𝓝∞ iff for every closed s ⊆ X with s compact, (↑)''sᶜ ∪ {∞} ∈ f.

Русский

Характеризация: f ≤ 𝓝∞ эквивалентно тому, что для каждого замкнутого s ⊆ X и компактного s выполняется (↑)''sᶜ ∪ {∞} ∈ f.

LaTeX

$$$f \le 𝓝_{∞} \iff \forall s\subset X, IsClosed(s) \land IsCompact(s) \rightarrow (↑) '' s^{c} \cup \{∞\} \in f$$$

Lean4

theorem tendsto_nhds_infty' {α : Type*} {f : OnePoint X → α} {l : Filter α} :
    Tendsto f (𝓝 ∞) l ↔ Tendsto f (pure ∞) l ∧ Tendsto (f ∘ (↑)) (coclosedCompact X) l := by
  simp [nhds_infty_eq, and_comm]

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