monotone_rpow_of_base_ge_one — Mathlib

English

If b ≥ 1, then x ↦ b^x is monotone (nondecreasing) on the real line.

Русский

Если b ≥ 1, то функция x ↦ b^x по R монотонно неубывает.

LaTeX

$$$1 \le b \Rightarrow \forall x,y \in \mathbb{R},\ x \le y \Rightarrow b^{x} \le b^{y}$$$

Lean4

theorem monotone_rpow_of_base_ge_one {b : ℝ} (hb : 1 ≤ b) : Monotone (b ^ · : ℝ → ℝ) :=
  by
  rcases lt_or_eq_of_le hb with hb | rfl
  case inl => exact (strictMono_rpow_of_base_gt_one hb).monotone
  case inr => intro _ _ _; simp

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