const_mul — Mathlib

English

If f grows polynomially, then c·f grows polynomially for any constant c.

Русский

Если f растёт полиномиально, то c·f растёт полиномиально для любого константного c.

LaTeX

$$$\\text{GrowsPolynomially}(f) \\Rightarrow \\text{GrowsPolynomially}(x \\mapsto c \\cdot f(x))$$$

Lean4

theorem const_mul {f : ℝ → ℝ} {c : ℝ} (hf : GrowsPolynomially f) : GrowsPolynomially fun x => c * f x :=
  GrowsPolynomially.mul growsPolynomially_const hf

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