strictAntiOn_rpow_Ioi_of_exponent_neg

English

For any r < 0, the function x ↦ x^r is strictly decreasing on (0, ∞).

Русский

Для любого r < 0 функция x ↦ x^r строго возрастает в отношении убывания на (0, ∞).

LaTeX

$$$ \forall r<0:\; \text{StrictAntiOn}(x \mapsto x^r)\text{ on }(0,\infty) $$$

Lean4

theorem strictAntiOn_rpow_Ioi_of_exponent_neg {r : ℝ} (hr : r < 0) : StrictAntiOn (fun (x : ℝ) => x ^ r) (Set.Ioi 0) :=
  fun _ ha _ _ hab => rpow_lt_rpow_of_exponent_neg ha hab hr

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