nhds_nhds — Mathlib

English

In a topological space X, for any x, 𝓝(𝓝 x) equals the iInf over open sets s containing x of 𝓟(Iic(𝓟 s)).

Русский

В топологическом пространстве X: 𝓝(𝓝 x) = ⨅ (s open, x ∈ s) 𝓟(Iic(𝓟 s)).

LaTeX

$$$\forall x:\, X,\; 𝓝(𝓝 x) = \bigwedge_{s:\ Set X} (IsOpen s) (x ∈ s) \; 𝓟(Iic(𝓟 s)).$$$

Lean4

theorem nhds_nhds (x : X) : 𝓝 (𝓝 x) = ⨅ (s : Set X) (_ : IsOpen s) (_ : x ∈ s), 𝓟 (Iic (𝓟 s)) := by
  simp only [(nhds_basis_opens x).nhds.eq_biInf, iInf_and, @iInf_comm _ (_ ∈ _)]

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