isLittleO_one_exp_comp — Mathlib

English

The constant function 1 is little-o of exp(f) along l if and only if f tends to +∞ along l.

Русский

Пусть 1 есть константа. Тогда 1 = o_l exp(f) тогда и только тогда, когда f(x) → +∞ вдоль l.

LaTeX

$$$ 1 = o_l(\exp \circ f) \iff \operatorname{Tendsto} f \ l\ atTop $$$

Lean4

theorem isLittleO_one_exp_comp {f : α → ℝ} : ((fun _ => 1 : α → ℝ) =o[l] fun x => exp (f x)) ↔ Tendsto f l atTop := by
  simp only [← exp_zero, isLittleO_exp_comp_exp_comp, sub_zero]

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