English
For partial relations r, l a filter, and x ∈ X, RTendsto' r l (nhds x) holds iff for every open s, x ∈ s implies r.preimage s ∈ l.
Русский
Для частого отношения r, фильтра l и точки x, RTendsto' r l (nhds x) эквивалентно тому, что для любого открытого s, x ∈ s → r.preimage s ∈ l.
LaTeX
$$$\\mathrm{RTendsto'}\\,r\\,l\\, (\\mathcal{N}(x)) \\iff \\forall s, \\mathrm{IsOpen}s \\to x \\in s \\to r.preimage 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.preimage s ∈ l :=
by
rw [rtendsto'_def]
apply all_mem_nhds_filter
apply SetRel.preimage_mono
