nhds_mkOfNhds — Mathlib

English

In a single element space, the neighborhood filter at a is determined by pure filters update; if l is above pure a, then nhds equals the updated pure filter at a.

Русский

В пространстве с одним элементом окрестности фиксируются через обновление фильтра; если l выше чистого фильтра при a, то окрестности совпадают с обновлённым чистым фильтром.

LaTeX

$$$nhds\\_mkOfNhds\\_single = \\text{update pure}(a,l).$$$

Lean4

theorem nhds_mkOfNhds (n : α → Filter α) (a : α) (h₀ : pure ≤ n) (h₁ : ∀ a, ∀ s ∈ n a, ∀ᶠ y in n a, s ∈ n y) :
    @nhds α (TopologicalSpace.mkOfNhds n) a = n a :=
  nhds_mkOfNhds_of_hasBasis (fun a ↦ (n a).basis_sets) h₀ h₁ _

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