nhds_infty_eq — Mathlib

English

The neighborhood filter at ∞ in OnePoint X is the join of the pushforward of coclosedCompact X and the pure ∞ filter.

Русский

Окрестности ∞ в OnePoint X равны объединению отображения coclosedCompact(X) и чистой ∞.

LaTeX

$$$\mathcal{N}(\infty) = (\operatorname{map}(\iota)(\operatorname{coclosedCompact}(X))) \sqcup \operatorname{pure}(\infty).$$$

Lean4

theorem nhds_infty_eq : 𝓝 (∞ : OnePoint X) = map (↑) (coclosedCompact X) ⊔ pure ∞ := by
  rw [← nhdsNE_infty_eq, nhdsNE_sup_pure]

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