English
Let X be a T1 topological space and let x ∈ X. If the neighborhood filter at x has a basis {s_i} with predicate p(i), then the intersection of all these basis sets equals the singleton {x}. In particular, the intersection of all neighborhoods forming a basis at x is exactly {x} in a T1 space.
Русский
Пусть X — топологическое пространство T1 и x ∈ X. Если фильтр окрестностей x имеет базис {s_i} с условием p(i), то пересечение всех этих множеств равно {x}. Иными словами, пересечение всех окрестностей базиса в x совпадает с единицей {x} в T1-пространстве.
LaTeX
$$$\displaystyle \bigcap_{i: \iota,\; p(i)} s(i) = \{ x \}$$$
Lean4
theorem biInter_basis_nhds [T1Space X] {ι : Sort*} {p : ι → Prop} {s : ι → Set X} {x : X} (h : (𝓝 x).HasBasis p s) :
⋂ (i) (_ : p i), s i = { x } := by rw [← h.ker, ker_nhds]
