tendsto_atTop — Mathlib

English

Two sequences are equivalent in asymptotics along l if and only if they both tend to atTop.

Русский

Две функции, эквивалентные по l, либо обе стремятся к бесконечности, либо нет.

LaTeX

$$$ u \\sim_{l} v \\Rightarrow (\\mathrm{Tendsto}\\;u\\ l\\ \\mathrm{atTop}) \\iff (\\mathrm{Tendsto}\\;v\\ l\\ \\mathrm{atTop}) $$$

Lean4

theorem tendsto_atTop [OrderTopology β] (huv : u ~[l] v) (hu : Tendsto u l atTop) : Tendsto v l atTop :=
  let ⟨φ, hφ, h⟩ := huv.symm.exists_eq_mul
  Tendsto.congr' h.symm (mul_comm u φ ▸ hu.atTop_mul_pos zero_lt_one hφ)

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