rpow_lt_rpow — Mathlib

English

If 0 ≤ x < y and z > 0, then x^z < y^z.

Русский

Если 0 ≤ x < y и z > 0, то x^z < y^z.

LaTeX

$$$ x^z < y^z, \quad 0 \le x < y,\ z > 0 $$$

Lean4

@[gcongr, bound]
theorem rpow_lt_rpow (hx : 0 ≤ x) (hxy : x < y) (hz : 0 < z) : x ^ z < y ^ z :=
  by
  rw [le_iff_eq_or_lt] at hx; rcases hx with hx | hx
  · rw [← hx, zero_rpow (ne_of_gt hz)]
    exact rpow_pos_of_pos (by rwa [← hx] at hxy) _
  · rw [rpow_def_of_pos hx, rpow_def_of_pos (lt_trans hx hxy), exp_lt_exp]
    exact mul_lt_mul_of_pos_right (log_lt_log hx hxy) hz

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