nhds_eq — Mathlib

English

In CofiniteTopology X, the neighborhood filter at x is the supremum of the pure filter at x and the cofinite filter on X.

Русский

В CofiniteTopology X окрестности точки x равны максимуму фильтра pure x и когонитивного фильтра cofinitе на X.

LaTeX

$$$$ \\mathcal{N}(x) = \\mathrm{pure}(x) \\sqcup \\mathrm{cofinite} $$$$

Lean4

theorem nhds_eq (x : CofiniteTopology X) : 𝓝 x = pure x ⊔ cofinite :=
  by
  ext U
  rw [mem_nhds_iff]
  constructor
  · rintro ⟨V, hVU, V_op, haV⟩
    exact mem_sup.mpr ⟨hVU haV, mem_of_superset (V_op ⟨_, haV⟩) hVU⟩
  · rintro ⟨hU : x ∈ U, hU' : Uᶜ.Finite⟩
    exact ⟨U, Subset.rfl, fun _ => hU', hU⟩

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