le_nhds_infty — Mathlib

English

The comap of nhds at ∞ along the one-point embedding equals the coclosedCompact X as a set, establishing a tight link between the boundary point and compact subsets of X.

Русский

Обратное изображение nhds(∞) вдоль вложения соответствует coclosedCompact(X).

LaTeX

$$$\operatorname{comap}(\operatorname{OnePoint}.some)(\mathcal{N}(\operatorname{OnePoint}.infty)) = \operatorname{coclosedCompact}(X)$$$

Lean4

theorem le_nhds_infty {f : Filter (OnePoint X)} :
    f ≤ 𝓝 ∞ ↔ ∀ s : Set X, IsClosed s → IsCompact s → (↑) '' sᶜ ∪ {∞} ∈ f := by
  simp only [hasBasis_nhds_infty.ge_iff, and_imp]

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