of_isEquivalent — Mathlib

English

If g grows polynomially and f is asymptotically equivalent to g, then f grows polynomially.

Русский

Если g растёт полиномиально, а f асимптотически эквивалентна g, то f растёт полиномиально.

LaTeX

$$$\\text{GrowsPolynomially}(g) \\to (f =_ {atTop} g) \\to \\text{GrowsPolynomially}(f)$$$

Lean4

theorem of_isEquivalent {f g : ℝ → ℝ} (hg : GrowsPolynomially g) (hf : f ~[atTop] g) : GrowsPolynomially f :=
  by
  have : f = g + (f - g) := by ext; simp
  rw [this]
  exact add_isLittleO hg hf

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