nhdsSet — Mathlib

English

The filter of neighborhoods of a subset s ⊆ X is the supremum of the neighborhood filters at its points.

Русский

Фильтр окрестностей множества s ⊆ X есть супремум фильтров окрестностей по точкам этого множества.

LaTeX

$$$nhdsSet(s) = \sup\{ nhds(x) : x \in s \}$$$

Lean4

/-- The filter of neighborhoods of a set in a topological space. -/
def nhdsSet (s : Set X) : Filter X :=
  sSup (nhds '' s)

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