rpow_le_self_of_le_one — Mathlib

English

If x ≤ 1, then x^z ≤ x for z ≥ 1. The power with exponent at least 1 does not exceed the base when the base is at most 1.

Русский

Если x ≤ 1, то x^z ≤ x для z ≥ 1.

LaTeX

$$$x \le 1 \land z \ge 1 \Rightarrow x^{z} \le x$$$

Lean4

theorem rpow_le_self_of_le_one {x : ℝ≥0} {z : ℝ} (hx : x ≤ 1) (h_one_le : 1 ≤ z) : x ^ z ≤ x :=
  by
  rcases eq_bot_or_bot_lt x with (rfl | (h : 0 < x))
  · have : z ≠ 0 := by linarith
    simp [this]
  nth_rw 2 [← NNReal.rpow_one x]
  exact NNReal.rpow_le_rpow_of_exponent_ge h hx h_one_le

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