congr — Mathlib

English

If two functions f1 and f2 agree pointwise, then any Tendsto f1 l1 l2, implies Tendsto f2 l1 l2.

Русский

Если функции f1 и f2 совпадают по каждому аргументу, то любой предел 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 \\Rightarrow \\mathrm{Tendsto} f_2\\ l_1\\ l_2)$$$

Lean4

theorem congr {f₁ f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β} (h : ∀ x, f₁ x = f₂ x) :
    Tendsto f₁ l₁ l₂ → Tendsto f₂ l₁ l₂ :=
  (tendsto_congr h).1

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