tendsto_rpow_atTop_of_base_lt_one

English

Let b be an extended nonnegative real with b < 1. Then as x tends to +∞, b^x tends to 0 in the extended nonnegative reals.

Русский

Пусть b ∈ ℝ≥0∞ и b < 1. Тогда при x → +∞, b^x стремится к 0 в ℝ≥0∞.

LaTeX

$$$\forall b \in \mathbb{R}_{\ge 0}^{\infty},\ b<1\ \Rightarrow\ \lim_{t \to +\infty} b^{t} = 0$$$

Lean4

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

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