tendsto_nhds — Mathlib

English

If u ~[l] v and Tendsto u l (nhds c), then Tendsto v l (nhds c).

Русский

Если u ~[l] v и u сходится к c вдоль l, тогда v сходится к c вдоль l.

LaTeX

$$u ~[l] v \Rightarrow (Tendsto u l (nhds c) \Rightarrow Tendsto v l (nhds c))$$

Lean4

theorem tendsto_nhds {c : β} (huv : u ~[l] v) (hu : Tendsto u l (𝓝 c)) : Tendsto v l (𝓝 c) :=
  by
  by_cases h : c = 0
  · subst c
    rw [← isLittleO_one_iff ℝ] at hu ⊢
    simpa using (huv.symm.isLittleO.trans hu).add hu
  · rw [← isEquivalent_const_iff_tendsto h] at hu ⊢
    exact huv.symm.trans hu

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