English
The neighborhood filter at a point a in the generated topology equals the infimum of principal filters over all sets s containing a and belonging to g.
Русский
Около точки a в топологии, порождённой, окрестности равны наименьшей нижней границе принципов над всеми множествами s, содержащими a и принадлежащими g.
LaTeX
$$$\\mathrm{nhds}(a) = \\bigwedge_{s \\ni a,\, s \\in g} \\mathcal{P}(s).$$$
Lean4
theorem nhds_generateFrom {g : Set (Set α)} {a : α} : @nhds α (generateFrom g) a = ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s :=
by
letI := generateFrom g
rw [nhds_def]
refine le_antisymm (biInf_mono fun s ⟨as, sg⟩ => ⟨as, .basic _ sg⟩) <| le_iInf₂ ?_
rintro s ⟨ha, hs⟩
induction hs with
| basic _ hs => exact iInf₂_le _ ⟨ha, hs⟩
| univ => exact le_top.trans_eq principal_univ.symm
| inter _ _ _ _ hs ht => exact (le_inf (hs ha.1) (ht ha.2)).trans_eq inf_principal
| sUnion _ _ hS =>
let ⟨t, htS, hat⟩ := ha
exact (hS t htS hat).trans (principal_mono.2 <| subset_sUnion_of_mem htS)
