English
Let α be a index set with a filter l, f : α → C(Y,Z), and g ∈ C(Y,Z). Then Tendsto f l (nhds g) holds iff for every compact K ⊆ Y and open U ⊆ Z, MapsTo g K U implies that eventually, MapsTo (f a) K U holds along l.
Русский
Пусть α — индексированное множество с фильтром l, f: α → C(Y,Z) и g ∈ C(Y,Z). Тогда Tendsto f l (nhds g) эквивало тому, что для всех компактных K ⊆ Y и открытых U ⊆ Z, если MapsTo g K U, то вдоль l выполняется условие MapsTo (f a) K U для почти всех a.
LaTeX
$$$ Tendsto\\; f\\; l\\; (\\mathcal{N}g) \\iff \\forall K,\\; IsCompact K \\to \\forall U,\\; IsOpen U \\to \\; MapsTo\\ g\\ K\\ U \\to \\forall^\\! a \\in l, MapsTo\\ (f\\ a)\\ K\\ U $$$
Lean4
theorem tendsto_nhds_compactOpen {l : Filter α} {f : α → C(Y, Z)} {g : C(Y, Z)} :
Tendsto f l (𝓝 g) ↔ ∀ K, IsCompact K → ∀ U, IsOpen U → MapsTo g K U → ∀ᶠ a in l, MapsTo (f a) K U := by
simp [nhds_compactOpen]
