English
A generic limit-of-a-relation predicate: RTendsto r l1 l2 holds if the r-core of every l2-neighborhood is an l1-neighborhood.
Русский
Обобщённое понятие предела по отношению: RTendsto r l1 l2 истинно, если для каждого окружения l2 ядро r по отношению к окружению l1.
LaTeX
$$$\mathrm{RTendsto}(r,l_1,l_2) := l_1.rmap r \leq l_2$$$
Lean4
/-- Generic "limit of a relation" predicate. `RTendsto r l₁ l₂` asserts that for every
`l₂`-neighborhood `a`, the `r`-core of `a` is an `l₁`-neighborhood. One generalization of
`Filter.Tendsto` to relations. -/
def RTendsto (r : SetRel α β) (l₁ : Filter α) (l₂ : Filter β) :=
l₁.rmap r ≤ l₂
