English
If two functions f1 and f2 are equal eventually with respect to a filter l1, then Tendsto f1 l1 l2 holds exactly when Tendsto f2 l1 l2 holds.
Русский
Если две функции f1 и f2 равны на хвосте относительно фильтра l1, то их пределы по l1 к l2 совпадают: Tendsto f1 l1 l2 эквивалентно Tendsto f2 l1 l2.
LaTeX
$$$\\forall f_1,f_2:\\alpha \\to \\beta, \\forall l_1:\\mathrm{Filter}(\\alpha), \\forall l_2:\\mathrm{Filter}(\\beta),\\; (f_1 =^{l_1} f_2) \\Rightarrow (\\mathrm{Tendsto} f_1\\ l_1\\ l_2 \\iff \\mathrm{Tendsto} f_2\\ l_1\\ l_2)$$$
Lean4
theorem tendsto_congr' {f₁ f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β} (hl : f₁ =ᶠ[l₁] f₂) :
Tendsto f₁ l₁ l₂ ↔ Tendsto f₂ l₁ l₂ := by rw [Tendsto, Tendsto, map_congr hl]
