powOrderIso — Mathlib

English

The map x ↦ x^n is an order isomorphism of ℝ≥0 onto itself when n ≠ 0.

Русский

Отображение x ↦ x^n при n ≠ 0 является порядковым изоморфизмом ℝ≥0 на ℝ≥0.

LaTeX

$$x ≤ y ⇔ x^n ≤ y^n and ∀z ≥ 0 ∃x ≥ 0, x^n = z, for n ≠ 0$$

Lean4

/-- `x ↦ x ^ n` as an order isomorphism of `ℝ≥0`. -/
def powOrderIso (n : ℕ) (hn : n ≠ 0) : ℝ≥0 ≃o ℝ≥0 :=
  StrictMono.orderIsoOfSurjective (fun x ↦ x ^ n) (fun x y h => pow_left_strictMonoOn₀ hn (zero_le x) (zero_le y) h) <|
    (continuous_id.pow _).surjective (tendsto_pow_atTop hn) <| by simpa [OrderBot.atBot_eq, pos_iff_ne_zero]

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