rpow_le_rpow_of_exponent_ge_of_imp

English

If 0 ≤ x ≤ 1 and z ≤ y and x = 0 implies y = 0 implies z = 0, then x^y ≤ x^z.

Русский

Пусть 0 ≤ x ≤ 1 и z ≤ y, и если x = 0, то обязательно y = 0 и z = 0; тогда x^y ≤ x^z.

LaTeX

$$$0 \le x \le 1 \land z \le y \land (x = 0 \rightarrow y = 0 \rightarrow z = 0) \rightarrow x^{y} \le x^{z}$$$

Lean4

/-- This is a more general but less convenient version of `rpow_le_rpow_of_exponent_ge`.
This version allows `x = 0`, so it explicitly forbids `x = y = 0`, `z ≠ 0`. -/
theorem rpow_le_rpow_of_exponent_ge_of_imp (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (hyz : z ≤ y) (h : x = 0 → y = 0 → z = 0) :
    x ^ y ≤ x ^ z := by
  rcases eq_or_lt_of_le hx0 with (rfl | hx0')
  · rcases eq_or_ne y 0 with rfl | hy0
    · rw [h rfl rfl]
    · rw [zero_rpow hy0]
      apply zero_rpow_nonneg
  · exact rpow_le_rpow_of_exponent_ge hx0' hx1 hyz

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