mem_nhds — Mathlib

English

If b is a topological basis, s ∈ b and a ∈ s, then s is a neighborhood of a.

Русский

Если b — топологическая база, и s ∈ b, a ∈ s, то s является окрестностью a.

LaTeX

$$mem_nhds {a : α} {s : Set α} {b : Set (Set α)} (hb : IsTopologicalBasis b) (hs : s ∈ b) (ha : a ∈ s) : s ∈ 𝓝 a$$

Lean4

protected theorem mem_nhds {a : α} {s : Set α} {b : Set (Set α)} (hb : IsTopologicalBasis b) (hs : s ∈ b) (ha : a ∈ s) :
    s ∈ 𝓝 a :=
  (hb.isOpen hs).mem_nhds ha

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