English
Let f: α → β. The statement Tendsto f l1 l2 is equivalent to l1 ≤ comap f l2. In other words, f preserves convergence exactly when every set in l2 pulls back to a set in l1.
Русский
Пусть f: α → β. Сходимость Tendsto f l1 l2 эквивалентна тому, что l1 ≤ comap f l2; то есть предел сохраняется тогда и только тогда, когда каждый элемент l2 вытягивается обратно в l1 через f.
LaTeX
$$$\\forall f:\\alpha \\to \\beta, \\forall l_1:\\mathrm{Filter}(\\alpha), \\forall l_2:\\mathrm{Filter}(\\beta),\\; \\mathrm{Tendsto} f\\ l_1\\ l_2 \\iff l_1 \\le \\mathrm{comap} f\\ l_2$$$
Lean4
theorem tendsto_iff_comap {f : α → β} {l₁ : Filter α} {l₂ : Filter β} : Tendsto f l₁ l₂ ↔ l₁ ≤ l₂.comap f :=
map_le_iff_le_comap
