strictMono_rpow_of_base_gt_one — Mathlib

English

Let b > 1. The function x ↦ b^x is strictly increasing on the real line.

Русский

Пусть b > 1. Функция x ↦ b^x по вещественным числам строго возрастает.

LaTeX

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

Lean4

theorem strictMono_rpow_of_base_gt_one {b : ℝ} (hb : 1 < b) : StrictMono (b ^ · : ℝ → ℝ) :=
  by
  simp_rw [Real.rpow_def_of_pos (zero_lt_one.trans hb)]
  exact exp_strictMono.comp <| StrictMono.const_mul strictMono_id <| Real.log_pos hb

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