English
The neighborhood filter at f in C(X,Y) has a basis described by finite families of compact-K and open-U data, with MapsTo constraints for f.
Русский
Окрестностная система в точке f в C(X,Y) имеет базис, задаваемый конечными наборами данных о компактных K и открытых U с ограничениями MapsTo для f.
LaTeX
$$$ (\\text{nhds}\\, f).\\text{HasBasis} \\bigl(\\lambda S : \\text{Set} (\\text{Set } X \\times \\text{Set } Y) \\to S.Finite \\wedge \\forall K U, (K,U) \\in S \\to IsCompact K \\wedge IsOpen U \\wedge MapsTo f K U\\bigr) \\bigl( \\bigcap_{KU \\in \\cdot} \\{ g : C(X,Y) \\mid MapsTo g KU.1 KU.2 \\} \\bigr) $$$
Lean4
protected theorem hasBasis_nhds (f : C(X, Y)) :
(𝓝 f).HasBasis (fun S : Set (Set X × Set Y) ↦ S.Finite ∧ ∀ K U, (K, U) ∈ S → IsCompact K ∧ IsOpen U ∧ MapsTo f K U)
(⋂ KU ∈ ·, {g : C(X, Y) | MapsTo g KU.1 KU.2}) :=
by
refine ⟨fun s ↦ ?_⟩
simp_rw [nhds_compactOpen, iInf_comm.{_, 0, _ + 1}, iInf_prod', iInf_and']
simp [mem_biInf_principal, and_assoc]
