English
The neighborhoods of x have a basis consisting of open sets that contain x.
Русский
Окрестности точки x имеют базу из открытых множеств, содержащих x.
LaTeX
$$$(\\mathcal N(x)) \\text{ has basis } (\\lambda s. x \\in s \\land \\text{IsOpen}(s)) \\; \\text{ with index } s$$$
Lean4
/-- The open sets containing `x` are a basis for the neighborhood filter. See `nhds_basis_opens'`
for a variant using open neighborhoods instead. -/
theorem nhds_basis_opens (x : X) : (𝓝 x).HasBasis (fun s : Set X => x ∈ s ∧ IsOpen s) fun s => s :=
by
rw [nhds_def]
exact
hasBasis_biInf_principal
(fun s ⟨has, hs⟩ t ⟨hat, ht⟩ =>
⟨s ∩ t, ⟨⟨has, hat⟩, IsOpen.inter hs ht⟩, ⟨inter_subset_left, inter_subset_right⟩⟩)
⟨univ, ⟨mem_univ x, isOpen_univ⟩⟩
