nhds_closure — Mathlib

English

If a basis for nhds x is given, then a basis for nhds x via closures of the basis elements exists.

Русский

Если дан базис для окрестностей x, то существует базис окрестностей x через замыкания элементов базиса.

LaTeX

$$$\forall X,\forall x,\text{basis } h: (nhds x).HasBasis p s \Rightarrow (nhds x).HasBasis p (\lambda i.\mathrm{closure}(s i))$$$

Lean4

theorem nhds_closure {ι : Sort*} {x : X} {p : ι → Prop} {s : ι → Set X} (h : (𝓝 x).HasBasis p s) :
    (𝓝 x).HasBasis p fun i => closure (s i) :=
  lift'_nhds_closure x ▸ h.lift'_closure

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