English
Let B be a family of filter bases B: α → FilterBasis α on a set α. Suppose every B(a) contains a; and suppose the following refinement condition: for every a and every n ∈ B(a) there exists n1 ∈ B(a) with n1 ⊆ n, and for every x′ ∈ n1 there exists n2 ∈ B(x′) with n2 ⊆ n. Then the neighborhood filter at a in the topology generated by the family of filters (B(x).filter) equals the filter (B(a).filter).
Русский
Пусть B: α → FilterBasis α — семейство баз фильтров на множество α. Пусть для каждого a выполняется a ∈ n для всех n ∈ B(a); и пусть выполняется уточняющее условие: для каждого a и каждого n ∈ B(a) существует n1 ∈ B(a) с n1 ⊆ n, и для каждого x′ ∈ n1 существует n2 ∈ B(x′) с n2 ⊆ n. Тогда окрестностный фильтр в точке a для топологии, порождаемой фильтрами (B(x).filter), равен фильтру (B(a).filter).
LaTeX
$$$\\mathrm{nhds}_{\\tau}(a) = (B(a)).\\mathrm{filter}$, where $\\tau = \\mathrm{mkOfNhds}(\\lambda x. (B(x)).\\mathrm{filter})$ and the hypotheses $h_0,h_1$ hold.$$
Lean4
theorem nhds_mkOfNhds_filterBasis (B : α → FilterBasis α) (a : α) (h₀ : ∀ x, ∀ n ∈ B x, x ∈ n)
(h₁ : ∀ x, ∀ n ∈ B x, ∃ n₁ ∈ B x, ∀ x' ∈ n₁, ∃ n₂ ∈ B x', n₂ ⊆ n) :
@nhds α (TopologicalSpace.mkOfNhds fun x => (B x).filter) a = (B a).filter :=
nhds_mkOfNhds_of_hasBasis (fun a ↦ (B a).hasBasis) h₀ h₁ a
