rpow_le_one_of_one_le_of_neg — Mathlib

English

If x ≥ 1 and z < 0, then x^{z} ≤ 1.

Русский

Если x ≥ 1 и z < 0, то x^z ≤ 1.

LaTeX

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

Lean4

theorem rpow_le_one_of_one_le_of_neg {x : ℝ≥0∞} {z : ℝ} (hx : 1 ≤ x) (hz : z < 0) : x ^ z ≤ 1 :=
  by
  cases x
  · simp [top_rpow_of_neg hz]
  · simp only [one_le_coe_iff] at hx
    simp [← coe_rpow_of_ne_zero (ne_of_gt (lt_of_lt_of_le zero_lt_one hx)),
      NNReal.rpow_le_one_of_one_le_of_nonpos hx (le_of_lt hz)]

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