congr' — Mathlib

English

If f1 and f2 are equal as functions, then 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 l_1:\\mathrm{Filter}(\\alpha), \\forall l_2:\\mathrm{Filter}(\\beta),\\; (f_1 = f_2) \\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 β} (hl : f₁ =ᶠ[l₁] f₂) (h : Tendsto f₁ l₁ l₂) :
    Tendsto f₂ l₁ l₂ :=
  (tendsto_congr' hl).1 h

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