rpow_le_rpow_of_exponent_le_or_ge

English

Let x,y,z ∈ ℝ. If either x ≥ 1 and y ≤ z, or 0 < x ≤ 1 and z ≤ y, then x^y ≤ x^z.

Русский

Пусть x,y,z ∈ ℝ. При условии либо x ≥ 1 и y ≤ z, либо 0 < x ≤ 1 и z ≤ y, выполняется x^y ≤ x^z.

LaTeX

$$$(1 \le x \land y \le z) \lor (0 < x \land x \le 1 \land z \le y) \Rightarrow x^{y} \le x^{z}$$$

Lean4

/-- Guessing rule for the `bound` tactic: when trying to prove `x ^ y ≤ x ^ z`, we can either assume
`1 ≤ x` or `0 < x ≤ 1`. -/
@[bound]
theorem rpow_le_rpow_of_exponent_le_or_ge {x y z : ℝ} (h : 1 ≤ x ∧ y ≤ z ∨ 0 < x ∧ x ≤ 1 ∧ z ≤ y) : x ^ y ≤ x ^ z :=
  by
  rcases h with ⟨x1, yz⟩ | ⟨x0, x1, zy⟩
  · exact Real.rpow_le_rpow_of_exponent_le x1 yz
  · exact Real.rpow_le_rpow_of_exponent_ge x0 x1 zy

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