rpow_le_rpow_of_exponent_le

Mathlib.Analysis.SpecialFunctions.Pow.Real

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

← MathLib Explorer

English

For y > 0, y ≤ x, and z ≤ 0, we have x^z ≤ y^z when x ≥ y > 0.

Русский

Для y > 0, y ≤ x и z ≤ 0 выполняется x^z ≤ y^z при x ≥ y > 0.

LaTeX

$$$ (0

Lean4

@[gcongr]
theorem rpow_le_rpow_of_exponent_le (hx : 1 ≤ x) (hyz : y ≤ z) : x ^ y ≤ x ^ z :=
  by
  repeat' rw [rpow_def_of_pos (lt_of_lt_of_le zero_lt_one hx)]
  rw [exp_le_exp]; exact mul_le_mul_of_nonneg_left hyz (log_nonneg hx)

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

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

Разделы

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

Аффилиация

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