tendsto_congr — Mathlib

English

If f1 and f2 are equal for all x, then Tendsto f1 l1 l2 is equivalent to Tendsto f2 l1 l2.

Русский

Если для всех x выполняется f1(x)=f2(x), то Tendsto f1 l1 l2 эквивалентно Tendsto f2 l1 l2.

LaTeX

$$$\\forall f_1,f_2:\\alpha \\to \\beta,\\; (\\forall x:\\alpha,\\; f_1(x)=f_2(x)) \\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 β} (h : ∀ x, f₁ x = f₂ x) :
    Tendsto f₁ l₁ l₂ ↔ Tendsto f₂ l₁ l₂ :=
  tendsto_congr' (univ_mem' h)

Похожие утверждения