antitone_rpow_of_base_le_one — Mathlib

English

If 0 < b ≤ 1, then x ↦ b^x is antitone (nonincreasing) on the real line.

Русский

Если 0 < b ≤ 1, то функция x ↦ b^x антимонотонна (не возрастает) по R.

LaTeX

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

Lean4

theorem antitone_rpow_of_base_le_one {b : ℝ} (hb₀ : 0 < b) (hb₁ : b ≤ 1) : Antitone (b ^ · : ℝ → ℝ) :=
  by
  rcases lt_or_eq_of_le hb₁ with hb₁ | rfl
  case inl => exact (strictAnti_rpow_of_base_lt_one hb₀ hb₁).antitone
  case inr => intro _ _ _; simp

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