English
Let X be a topological space and x ∈ X. The neighborhood filter at x has a basis consisting of open neighborhoods of x; equivalently, every neighborhood of x contains an open neighborhood of x.
Русский
Пусть X — топологическое пространство и x ∈ X. Фильтр окрестностей в x имеет базис, состоящий из открытых окрестностей x; эквивалентно: любая окрестность x содержит открытую окрестность x.
LaTeX
$$$\\forall x,\\ \\forall U \\in \\mathcal N_x\\;\\exists V\\;\\bigl( IsOpen(V) \\land x \\in V \\land V \\subseteq U \\bigr).$$$
Lean4
/-- The open neighborhoods of `x` are a basis for the neighborhood filter. See `nhds_basis_opens`
for a variant using open sets around `x` instead. -/
theorem nhds_basis_opens' (x : X) : (𝓝 x).HasBasis (fun s : Set X => s ∈ 𝓝 x ∧ IsOpen s) fun x => x :=
by
convert nhds_basis_opens x using 2
exact and_congr_left_iff.2 IsOpen.mem_nhds_iff
