English
For TopologicalSpace β, a map f: α → β, a ∈ α, and l a filter on α, the function f is continuous from nhdsAdjoint a l to the codomain iff f tends to nhds at f(a) along l.
Русский
Для топологических пространств β, отображения f: α → β, точки a ∈ α и фильтра l на α непрерывность f относительно nhdsAdjoint эквивалентна тому, что f стремится к nhds(f(a)) вдоль l.
LaTeX
$$$\\text{Continuous}[\\mathrm{nhdsAdjoint}\\ a\\ l, \\_ ]\n f \\iff \\operatorname{Tendsto} f\\ l\\ (\\mathcal{N}(f\\ a)).$$$
Lean4
theorem continuous_nhdsAdjoint_dom [TopologicalSpace β] {f : α → β} {a : α} {l : Filter α} :
Continuous[nhdsAdjoint a l, _] f ↔ Tendsto f l (𝓝 (f a)) := by
simp_rw [continuous_iff_le_induced, gc_nhds _ _, nhds_induced, tendsto_iff_comap]
