expGrowthInf_top

Mathlib.Analysis.Asymptotics.ExpGrowth

URI: https://scilib.ai/kg/mathlib#ExpGrowth.expGrowthInf_top

English

If b ≠ 0 and b ≠ ∞, then expGrowthInf (n ↦ b) = 0.

Русский

Если b ≠ 0 и b ≠ ∞, то expGrowthInf (постоянная b) = 0.

LaTeX

$$$b \neq 0 \land b \neq \infty \Rightarrow \expGrowthInf(\lambda n. b) = 0$$$

Lean4

theorem expGrowthInf_top : expGrowthInf ⊤ = ⊤ :=
  by
  rw [← linearGrowthInf_top, expGrowthInf_def]
  rfl

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

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

Разделы

Аффилиация

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