rpow_def_of_pos — Mathlib

English

For x ≥ 0 and y ∈ ℝ, x^y equals piecewise exp(log x · y) with the x=0 case handled as above.

Русский

Для x ≥ 0 и y ∈ ℝ, x^y равно кусочно-заданной формуле через exp(log x · y) с учетом случая x=0.

LaTeX

$$$$ x^y = \\begin{cases}1 & x=0 \\land y=0, \\\\ 0 & x=0 \\land y \\neq 0, \\\\ e^{\\log x \\\\cdot y} & x>0. \\end{cases} $$$$

Lean4

theorem rpow_def_of_pos {x : ℝ} (hx : 0 < x) (y : ℝ) : x ^ y = exp (log x * y) := by
  rw [rpow_def_of_nonneg (le_of_lt hx), if_neg (ne_of_gt hx)]

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