English
For a relation r, l a filter, and x ∈ X, PTendsto r l (nhds x) is equivalent to the same open-set criterion as RTendsto: for all open s containing x, r.core s ∈ l.
Русский
Для отношения r, фильтра l и точки x, PTendsto r l (nhds x) эквивалентно тому же условию для открытых множеств: для всех открытых s, содержащих x, ядро r в s принадлежит l.
LaTeX
$$$\\mathrm{PTendsto}\\,r\\,l\\,(\\mathcal{N}(x)) \\iff \\forall s, \\mathrm{IsOpen}s \\to x \\in s \\to r\\.core\\,s \\in l$$$
Lean4
theorem ptendsto_nhds {f : Y →. X} {l : Filter Y} {x : X} : PTendsto f l (𝓝 x) ↔ ∀ s, IsOpen s → x ∈ s → f.core s ∈ l :=
rtendsto_nhds
