English
Let r be a relation between Y and X, l a filter on Y, and x ∈ X. Then RTendsto r l (nhds x) holds iff for every open set s containing x, the core of s under r belongs to l.
Русский
Пусть r — отношение между Y и X, l — фильтр на Y, и x ∈ X. Тогда RTendsto r l (nhds x) эквивалентно тому, что для каждого открытого множества s, содержащего x, ядро s по отношению r принадлежит l.
LaTeX
$$$\\mathrm{RTendsto}\\,r\\,l\\, (\\mathcal{N}(x)) \\iff \\forall s, \\mathrm{IsOpen}\\,s \\to x \\in s \\to r\\mathrm{.core}\\,s \\in l$$$
Lean4
theorem rtendsto_nhds {r : SetRel Y X} {l : Filter Y} {x : X} :
RTendsto r l (𝓝 x) ↔ ∀ s, IsOpen s → x ∈ s → r.core s ∈ l :=
all_mem_nhds_filter _ _ (fun _s _t => id) _
