rpow_pos — Mathlib

English

If x > 0 and p is any real, then x^p > 0. Positive base with any real exponent yields a positive result.

Русский

Если x > 0 и p — любое действительное, то x^p > 0. Положительная база даёт положительную степень.

LaTeX

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

Lean4

theorem rpow_pos {p : ℝ} {x : ℝ≥0} (hx_pos : 0 < x) : 0 < x ^ p :=
  by
  have rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p :=
    by
    intro p hp_pos
    rw [← zero_rpow hp_pos.ne']
    exact rpow_lt_rpow hx_pos hp_pos
  rcases lt_trichotomy (0 : ℝ) p with (hp_pos | rfl | hp_neg)
  · exact rpow_pos_of_nonneg hp_pos
  · simp only [zero_lt_one, rpow_zero]
  · rw [← neg_neg p, rpow_neg, inv_pos]
    exact rpow_pos_of_nonneg (neg_pos.mpr hp_neg)

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