English
The neighborhood filter at a continuous map f is the infimum over all compact K and open U with MapsTo f K U of the principal filter generated by {g : C(X,Y) | MapsTo g K U}.
Русский
filters 𝒩(f) равен пересечению по всем компактным K и открытым U с условием MapsTo f K U и базой, задаваемой множеством {g : C(X,Y) | MapsTo g K U}.
LaTeX
$$$ \\mathcal{N}f = \\bigwedge_{K,\\,IsCompact K} \\bigwedge_{U,\\,IsOpen U} \\bigl( \\mathcal{P}\\{ g : C(X,Y) \\mid MapsTo g K U \\} \\bigr) $$$
Lean4
theorem nhds_compactOpen (f : C(X, Y)) :
𝓝 f =
⨅ (K : Set X) (_ : IsCompact K) (U : Set Y) (_ : IsOpen U) (_ : MapsTo f K U), 𝓟 {g : C(X, Y) | MapsTo g K U} :=
by
simp_rw [compactOpen_eq, nhds_generateFrom, mem_setOf_eq, @and_comm (f ∈ _), iInf_and, ← image_prod, iInf_image,
biInf_prod, mem_setOf_eq]
