English
For a topological space X and a point x ∈ X, the neighborhood filter at x, nhds x, is the infimum of the principal filters of all open sets containing x.
Русский
Для топологического пространства X и точки x ∈ X фильтр окрестностей nhds x является наименьшим фильтром, содержащим все окрестности точки x; эквивалентно наименьшему пределу принципиальных фильтров всех открытых множест x, содержащих x.
LaTeX
$$$nhds(x) = \inf\{ \mathcal{P}(U) : U \subseteq X,\ IsOpen U,\ x \in U \}$$$
Lean4
/-- A set is called a neighborhood of `x` if it contains an open set around `x`. The set of all
neighborhoods of `x` forms a filter, the neighborhood filter at `x`, is here defined as the
infimum over the principal filters of all open sets containing `x`. -/
def nhds :=
val_proj @wrapped✝.{}
