English
If a neighborhood basis exists with given sets s(a,i) and p(a,i), then nhds in the mkOfNhds topology equals the intersection of principal filters on those sets.
Русский
Если существует база окрестностей с множествами s(a,i) и условиям p(a,i), то окрестности в mkOfNhds совпадают с пересечением соответствующих принципиальных фильтров.
LaTeX
$$$\\text{nhds in }(\\mathrm{mkOfNhds}(n)) a = \\bigwedge_{i} \\mathcal{P}(s(a,i)).$$$
Lean4
theorem nhds_mkOfNhds_of_hasBasis {n : α → Filter α} {ι : α → Sort*} {p : ∀ a, ι a → Prop} {s : ∀ a, ι a → Set α}
(hb : ∀ a, (n a).HasBasis (p a) (s a)) (hpure : ∀ a i, p a i → a ∈ s a i)
(hopen : ∀ a i, p a i → ∀ᶠ x in n a, s a i ∈ n x) (a : α) : @nhds α (.mkOfNhds n) a = n a :=
by
let t : TopologicalSpace α := .mkOfNhds n
apply le_antisymm
· intro U hU
replace hpure : pure ≤ n := fun x ↦ (hb x).ge_iff.2 (hpure x)
refine mem_nhds_iff.2 ⟨{x | U ∈ n x}, fun x hx ↦ hpure x hx, fun x hx ↦ ?_, hU⟩
rcases (hb x).mem_iff.1 hx with ⟨i, hpi, hi⟩
exact (hopen x i hpi).mono fun y hy ↦ mem_of_superset hy hi
· exact (nhds_basis_opens a).ge_iff.2 fun U ⟨haU, hUo⟩ ↦ hUo a haU
