English
The kernel of the neighborhood filter of a set s is the intersection of all its neighborhoods.
Русский
Ядро фильтра окрестностей множества s есть пересечение всех его окрестностей.
LaTeX
$$$nhdsKer(s) = \bigcap_{U \in 𝓝ˢ s} U$$$
Lean4
/-- The *neighborhoods kernel* of a set is the intersection of all its neighborhoods. In an
Alexandrov-discrete space, this is the smallest neighborhood of the set. -/
def nhdsKer (s : Set X) : Set X :=
(𝓝ˢ s).ker