div — Mathlib

English

If f and g both grow polynomially, then f/g grows polynomially.

Русский

Если обе функции f и g растут полиномиально, то их отношение f/g растёт полиномиально.

LaTeX

$$$\\text{GrowsPolynomially}(f) \\land \\text{GrowsPolynomially}(g) \\Rightarrow \\text{GrowsPolynomially}(x \\mapsto \\tfrac{f(x)}{g(x)})$$$

Lean4

protected theorem div {f g : ℝ → ℝ} (hf : GrowsPolynomially f) (hg : GrowsPolynomially g) :
    GrowsPolynomially fun x => f x / g x :=
  by
  have : (fun x => f x / g x) = fun x => f x * (g x)⁻¹ := by ext; rw [div_eq_mul_inv]
  rw [this]
  exact GrowsPolynomially.mul hf (GrowsPolynomially.inv hg)

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