nhds_basis_closure — Mathlib

English

If B is a topological basis, then nhds basis can be chosen with closures of basis elements around x.

Русский

Если B — топологический базис, то окрестностная база может быть взята из замыкaний элементов базиса вокруг x.

LaTeX

$$$\forall {X} {x} (hB : IsTopologicalBasis B), (nhds x).HasBasis (fun s => x \in s ∧ s ∈ B) closure$$$

Lean4

theorem nhds_basis_closure {B : Set (Set X)} (hB : IsTopologicalBasis B) (x : X) :
    (𝓝 x).HasBasis (fun s : Set X => x ∈ s ∧ s ∈ B) closure := by
  simpa only [and_comm] using hB.nhds_hasBasis.nhds_closure

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