tendsto_rpow_atBot_of_one_lt_base

English

Let b > 1 in ENNReal. Then as x tends to -∞, b^x tends to 0 in ENNReal.

Русский

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

LaTeX

$$$\forall b > 1\ (b \in \mathbb{R}_{\ge 0}^{\infty})\ \Rightarrow\ \lim_{t \to -\infty} b^{t} = 0$$$

Lean4

theorem tendsto_rpow_atBot_of_one_lt_base {b : ℝ≥0∞} (hb : 1 < b) :
    Filter.Tendsto (b ^ · : ℝ → ℝ≥0∞) Filter.atBot (𝓝 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_atBot _ _
  · rw [EReal.bot_mul_of_pos (zero_lt_log_iff.2 hb)]
  all_goals simp

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