isEquivalent_const_iff_tendsto — Mathlib

English

If u ~[l] v and u tends to c along l, then v tends to c along l.

Русский

Если u эквивалентна v вдоль l и u стремится к c вдоль l, то и v стремится к c вдоль l.

LaTeX

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

Lean4

theorem isEquivalent_const_iff_tendsto {c : β} (h : c ≠ 0) : u ~[l] const _ c ↔ Tendsto u l (𝓝 c) :=
  by
  simp +unfoldPartialApp only [IsEquivalent, const, isLittleO_const_iff h]
  constructor <;> intro h
  · have := h.sub (tendsto_const_nhds (x := -c))
    simp only [Pi.sub_apply, sub_neg_eq_add, sub_add_cancel, zero_add] at this
    exact this
  · have := h.sub (tendsto_const_nhds (x := c))
    rwa [sub_self] at this

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