English
The exponential function is used as a partial homeomorphism between the real line and the positive reals, with the natural logarithm as its inverse: exp: R → (0,∞) and log: (0,∞) → R, with log the inverse of exp on appropriate domains.
Русский
Функция экспоненты образует частичную гомоморфизм между вещественной прямой и множеством положительных вещественных чисел, причём логарифм является её обратной. exp: R → (0,∞), log: (0,∞) → R, и log является обратной к exp на соответствующих областях.
LaTeX
$$$$ \\exp: \\mathbb{R} \\to (0,\\infty) \\quad \\text{and} \\quad \\log: (0,\\infty) \\to \\mathbb{R}, \\quad \\log(\\exp x) = x, \\quad \\exp(\\log y) = y \\ (y>0). $$$$
Lean4
/-- `Real.exp` as an `OpenPartialHomeomorph` with `source = univ` and `target = {z | 0 < z}`. -/
@[simps]
noncomputable def expPartialHomeomorph : OpenPartialHomeomorph ℝ ℝ
where
toFun := Real.exp
invFun := Real.log
source := univ
target := Ioi (0 : ℝ)
map_source' x _ := exp_pos x
map_target' _ _ := mem_univ _
left_inv' _ _ := by simp
right_inv' _ hx := exp_log hx
open_source := isOpen_univ
open_target := isOpen_Ioi
continuousOn_toFun := continuousOn_exp
continuousOn_invFun x hx := (continuousAt_log (ne_of_gt hx)).continuousWithinAt
