English
For x ≠ 0, the map y ↦ y^x is bijective on ENNReal.
Русский
Для x ≠ 0 отображение y ↦ y^x биективно на ℝ≥0∞.
LaTeX
$$$$ \\forall x ∈ \\mathbb{R}, x \\neq 0 \\rightarrow \\text{Bijective}(y \\mapsto y^x). $$$$
Lean4
/-- The real power function `x ^ y`, defined as the real part of the complex 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`. For `x < 0`, the definition is somewhat arbitrary as it depends on the choice of a complex
determination of the logarithm. With our conventions, it is equal to `exp (y log x) cos (π y)`. -/
noncomputable def rpow (x y : ℝ) :=
((x : ℂ) ^ (y : ℂ)).re
