add_const_of_norm_tendsto_atTop — Mathlib

English

If u is asymptotically equivalent to v and the norm of v tends to infinity along l, then c + u is asymptotically equivalent to v.

Русский

Если u эквивалентно v по l и ||v|| → ∞ по l, то c + u эквивалентно v по l.

LaTeX

$$$ (u \\sim_{l} v) \\land (\\ Tendsto (\\|v\\|) l \\; atTop) \\Rightarrow (\\lambda x. c + u(x)) \\sim_{l} v $$$

Lean4

theorem add_const_of_norm_tendsto_atTop {c : β} (huv : u ~[l] v) (hv : Tendsto (norm ∘ v) l atTop) : (u · + c) ~[l] v :=
  huv.add_isLittleO <| isLittleO_const_left.mpr (Or.inr hv)

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