rpow_pos — Mathlib

English

If x > 0 and p is real, then x^{p} > 0.

Русский

Если x > 0 и p произвольная, то x^p > 0.

LaTeX

$$$ x > 0 \\Rightarrow x^{p} > 0 $$$

Lean4

theorem rpow_pos {p : ℝ} {x : ℝ≥0∞} (hx_pos : 0 < x) (hx_ne_top : x ≠ ⊤) : 0 < x ^ p :=
  by
  rcases lt_or_ge 0 p with hp_pos | hp_nonpos
  · exact rpow_pos_of_nonneg hx_pos (le_of_lt hp_pos)
  · rw [← neg_neg p, rpow_neg, ENNReal.inv_pos]
    exact rpow_ne_top_of_nonneg (Right.nonneg_neg_iff.mpr hp_nonpos) hx_ne_top

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