rpow_le_one_of_one_le_of_nonpos

Mathlib.Analysis.SpecialFunctions.Pow.Real

URI: https://scilib.ai/kg/mathlib#Real.rpow_le_one_of_one_le_of_nonpos

← MathLib Explorer

English

If r ≤ 0, then x^r is antitone on (0, ∞).

Русский

Если r ≤ 0, то x^r антимонотно на (0, ∞).

LaTeX

$$$ r \le 0 \Rightarrow \text{AntitoneOn}(x \mapsto x^r)(\mathbb{I}_{(0,\infty)}) $$$

Lean4

theorem rpow_le_one_of_one_le_of_nonpos {x z : ℝ} (hx : 1 ≤ x) (hz : z ≤ 0) : x ^ z ≤ 1 :=
  by
  convert rpow_le_rpow_of_exponent_le hx hz
  exact (rpow_zero x).symm

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru