English
The relation-based limit predicate RTendsto is characterized by a lattice ordering: RTendsto r l1 l2 holds precisely when l1 is less than or equal to the r-comap of l2 along r.
Русский
Условия предела через отношение: RTendsto r l1 l2 эквивалентно l1 ≤ l2.rcomap r.
LaTeX
$$$ \\mathrm{RTendsto}(r)\\, l_1\\, l_2 \\quad\\Longleftrightarrow\\quad l_1 \\le l_2.\\mathrm{rcomap}(r) $$$
Lean4
theorem rtendsto_iff_le_rcomap (r : SetRel α β) (l₁ : Filter α) (l₂ : Filter β) : RTendsto r l₁ l₂ ↔ l₁ ≤ l₂.rcomap r :=
by
rw [rtendsto_def]
simp_rw [← l₂.mem_sets]
constructor
· simpa [Filter.le_def, rcomap, SetRel.mem_image] using fun h s t tl₂ => mem_of_superset (h t tl₂)
· simpa [Filter.le_def, rcomap, SetRel.mem_image] using fun h t tl₂ => h _ t tl₂ Set.Subset.rfl
