rpow_def_of_nonneg — Mathlib

English

Let x ≥ 0. Then x^y equals 1 if y=0 and x>0, else exp(log x · y); if x=0 and y≠0 then 0.

Русский

Пусть x ≥ 0. Тогда x^y = 1 если y=0 и x=0, иначе exp(log x · y); если x=0 и y≠0, тогда 0.

LaTeX

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

Lean4

theorem rpow_def_of_nonneg {x : ℝ} (hx : 0 ≤ x) (y : ℝ) :
    x ^ y = if x = 0 then if y = 0 then 1 else 0 else exp (log x * y) := by simp only [rpow_def, Complex.cpow_def];
  split_ifs <;>
    simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul, (Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re,
      Complex.ofReal_eq_zero]

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