tendsto_rpow_atTop_of_one_lt_base

English

If 1 < b in ENNReal, then the map x ↦ b^x tends to top as x → atTop.

Русский

Если b > 1 в ENNReal, то функция x ↦ b^x стремится к верхней границе при x → atTop.

LaTeX

$$∀ {b : ENNReal}, 1 < b → Tendsto (fun x => b^x) atTop (nhds ⊤)$$

Lean4

theorem tendsto_rpow_atTop_of_one_lt_base {b : ℝ≥0∞} (hb : 1 < b) :
    Filter.Tendsto (b ^ · : ℝ → ℝ≥0∞) Filter.atTop (𝓝 ⊤) :=
  by
  simp_rw [ENNReal.rpow_eq_exp_mul_log]
  refine EReal.tendsto_exp_nhds_top_nhds_top.comp ?_
  convert EReal.Tendsto.mul_const tendsto_coe_atTop _ _
  · rw [EReal.top_mul_of_pos (zero_lt_log_iff.2 hb)]
  all_goals simp

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