strictAnti_rpow_of_base_lt_one — Mathlib

English

If 0 < b < 1, then x ↦ b^x is strictly decreasing on the real line.

Русский

Если 0 < b < 1, то функция x ↦ b^x строго убывaет по R.

LaTeX

$$$0 < b < 1 \Rightarrow \forall x,y \in \mathbb{R},\ x < y \Rightarrow b^{x} > b^{y}$$$

Lean4

theorem strictAnti_rpow_of_base_lt_one {b : ℝ} (hb₀ : 0 < b) (hb₁ : b < 1) : StrictAnti (b ^ · : ℝ → ℝ) :=
  by
  simp_rw [Real.rpow_def_of_pos hb₀]
  exact exp_strictMono.comp_strictAnti <| StrictMono.const_mul_of_neg strictMono_id <| Real.log_neg hb₀ hb₁

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