English
There is an order isomorphism NNReal ≃o NNReal given by y ↦ y^x for a fixed x with x > 0.
Русский
Существуют отображение-изоморфизм порядка NNReal ≃o NNReal, задаваемое y ↦ y^x при фиксированном x > 0.
LaTeX
$$$x\\in\\mathbb{R},\\; x>0 \\implies \\mathbb{NNReal} \\;\\xrightarrow{\\;\\; y \\mapsto y^x \\;\\;} \\mathbb{NNReal}$ является упорядоченным изоморфизмом.$$
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]
