hasBasis_nhds_infty — Mathlib

English

The neighborhood system at ∞ in OnePoint X has a basis consisting of sets of the form (i''sᶜ) ∪ {∞} where s is closed and compact in X, together with the union with ∞.

Русский

У фильтра окрестностей ∞ в OnePoint X имеется базис из множеств вида (i''sᶜ) ∪ {∞}, где s замкнуто и компактно в X, и их объединение с ∞.

LaTeX

$$$(\mathcal{N}_{\infty}) .HasBasis (\lambda s : Set X \to IsClosed s \land IsCompact s) (\lambda s \to (\uparrow) '' s^c \cup \{\infty\})$$$

Lean4

theorem hasBasis_nhds_infty :
    (𝓝 (∞ : OnePoint X)).HasBasis (fun s : Set X => IsClosed s ∧ IsCompact s) fun s => (↑) '' sᶜ ∪ {∞} :=
  by
  rw [nhds_infty_eq]
  exact (hasBasis_coclosedCompact.map _).sup_pure _

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