growsPolynomially_const

Mathlib.Computability.AkraBazzi.GrowsPolynomially

URI: https://scilib.ai/kg/mathlib#AkraBazziRecurrence.growsPolynomially_const

← MathLib Explorer

English

A constant function grows polynomially.

Русский

Постоянная функция растёт полиномиально.

LaTeX

$$$\\text{GrowsPolynomially}(x \\mapsto c)$$$

Lean4

theorem growsPolynomially_const {c : ℝ} : GrowsPolynomially (fun _ => c) :=
  by
  refine fun _ _ => ⟨1, by norm_num, 1, by norm_num, ?_⟩
  filter_upwards [] with x
  simp

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru