English
The predicate RTendsto' expresses limit along a relation: it holds when the l1-neighborhoods of a set are mapped into l2-neighborhoods via the relation r.
Русский
Предикат RTendsto' выражает предел относительно отношения: он истинно, если окрестности l1 соответствуют окрестностям l2 через отношение r.
LaTeX
$$$ \\mathrm{RTendsto}'(r, l_1, l_2) \\iff l_1 \\le l_2.rcomap' r $$$
Lean4
/-- Generic "limit of a relation" predicate. `RTendsto' r l₁ l₂` asserts that for every
`l₂`-neighborhood `a`, the `r`-preimage of `a` is an `l₁`-neighborhood. One generalization of
`Filter.Tendsto` to relations. -/
def RTendsto' (r : SetRel α β) (l₁ : Filter α) (l₂ : Filter β) :=
l₁ ≤ l₂.rcomap' r
