rpow — Mathlib

English

For NNReal x > 0 and real y,z, x^{y+z} = x^y x^z, i.e., the power is additive in the exponent when the base is positive.

Русский

Пусть x ∈ ℝ≥0 и x > 0; для любых y,z ∈ ℝ выполняется x^{y+z} = x^y x^z, то есть показатель степени аддитивен по сумме.

LaTeX

$$$\\displaystyle x^{\,y+z} = x^{\,y} \\cdot x^{\,z} \\quad (x>0)$$

Lean4

/-- The nonnegative real power function `x^y`, defined for `x : ℝ≥0` and `y : ℝ` as the
restriction of the real power function. For `x > 0`, it is equal to `exp (y log x)`. For `x = 0`,
one sets `0 ^ 0 = 1` and `0 ^ y = 0` for `y ≠ 0`. -/
noncomputable def rpow (x : ℝ≥0) (y : ℝ) : ℝ≥0 :=
  ⟨(x : ℝ) ^ y, Real.rpow_nonneg x.2 y⟩

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