English
For a fixed y>0, the map x → x^y is an order isomorphism of ENNReal onto itself, with inverse x → x^{1/y}.
Русский
Для фиксированного y>0 отображение x → x^y является упорядоченным изоморфизмом ENNReal в сам себя; обратное отображение задается как x → x^{1/y}.
LaTeX
$$$$\text{For } y>0,\; x \mapsto x^{y} \text{ is an order isomorphism with inverse } x \mapsto x^{1/y}. $$$$
Lean4
/-- Bundles `fun x : ℝ≥0∞ => x ^ y` into an order isomorphism when `y : ℝ` is positive,
where the inverse is `fun x : ℝ≥0∞ => x ^ (1 / y)`. -/
@[simps! apply]
def orderIsoRpow (y : ℝ) (hy : 0 < y) : ℝ≥0∞ ≃o ℝ≥0∞ :=
(strictMono_rpow_of_pos hy).orderIsoOfRightInverse (fun x => x ^ y) (fun x => x ^ (1 / y)) fun x =>
by
dsimp
rw [← rpow_mul, one_div_mul_cancel hy.ne.symm, rpow_one]
