nhdsNE_infty_eq — Mathlib

English

The neighborhood filter at ∞ within the punctured neighborhood equals the pushforward of the coclosed compact filter from X.

Русский

Окрестности ∞ внутри удаленного от ∞ множества равны отображению фильтра coclosedCompact из X.

LaTeX

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

Lean4

theorem nhdsNE_infty_eq : 𝓝[≠] (∞ : OnePoint X) = map (↑) (coclosedCompact X) :=
  by
  refine (nhdsWithin_basis_open ∞ _).ext (hasBasis_coclosedCompact.map _) ?_ ?_
  · rintro s ⟨hs, hso⟩
    refine ⟨_, (isOpen_iff_of_mem hs).mp hso, ?_⟩
    simp
  · rintro s ⟨h₁, h₂⟩
    refine ⟨_, ⟨mem_compl infty_notMem_image_coe, isOpen_compl_image_coe.2 ⟨h₁, h₂⟩⟩, ?_⟩
    simp [compl_image_coe, ← diff_eq]

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