expOrderIso — Mathlib

English

The exponential map is an order isomorphism from ℝ onto (0, ∞).

Русский

Экспоненциальная карта устанавливает биекцию в виде порядка между ℝ и (0, ∞).

LaTeX

$$$\\exp : \\mathbb{R} \\to (0,\\infty) \\text{ is an order isomorphism}. $$$

Lean4

/-- `Real.exp` as an order isomorphism between `ℝ` and `(0, +∞)`. -/
def expOrderIso : ℝ ≃o Ioi (0 : ℝ) :=
  StrictMono.orderIsoOfSurjective _ (exp_strictMono.codRestrict exp_pos) <|
    (continuous_exp.subtype_mk _).surjective (by rw [tendsto_Ioi_atTop]; simp only [tendsto_exp_atTop])
      (by rw [tendsto_Ioi_atBot]; simp only [tendsto_exp_atBot_nhdsGT])

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