antitoneOn_rpow_Ioi_of_exponent_nonpos

English

If r ≤ 0, then x^r is antitone on the positive reals.

Русский

Если r ≤ 0, то x^r антимонотно на положительных вещественных числах.

LaTeX

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

Lean4

theorem antitoneOn_rpow_Ioi_of_exponent_nonpos {r : ℝ} (hr : r ≤ 0) : AntitoneOn (fun (x : ℝ) => x ^ r) (Set.Ioi 0) :=
  fun _ ha _ _ hab => rpow_le_rpow_of_exponent_nonpos ha hab hr

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