of_nhds — Mathlib

English

If every point has a neighborhood from S, then the topology is generated by the restrictions of S.

Русский

Если каждый точке пространства имеется окрестность из S, то топология задается ограничениями на множества S.

LaTeX

$$$ (\\forall x, \\exists s \\in S, s \\in \\mathcal{N}(x)) \\to \\text{IsCoherentWith } S $$$

Lean4

/-- If each point of the space has a neighborhood from the family `S`,
then the topology is generated by its restrictions to the sets of `S`. -/
theorem of_nhds (h : ∀ x, ∃ s ∈ S, s ∈ 𝓝 x) : IsCoherentWith S :=
  of_continuous_prop fun _f hf ↦
    continuous_iff_continuousAt.2 fun x ↦
      let ⟨s, hsS, hsx⟩ := h x
      (hf s hsS).continuousAt hsx

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