nhdsKer — Mathlib

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

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