English
The real logarithm maps positive real numbers onto all real numbers; i.e., log: (0, ∞) → ℝ is surjective.
Русский
Логарифм отображает положительные числа на всю множества ℝ; то есть log:(0, ∞) → ℝ сюръективен.
LaTeX
$$SurjOn(Real.log, (0, ∞), ℝ)$$
Lean4
/-- The real logarithm function, equal to the inverse of the exponential for `x > 0`,
to `log |x|` for `x < 0`, and to `0` for `0`. We use this unconventional extension to
`(-∞, 0]` as it gives the formula `log (x * y) = log x + log y` for all nonzero `x` and `y`, and
the derivative of `log` is `1/x` away from `0`. -/
@[pp_nodot]
noncomputable def log (x : ℝ) : ℝ :=
if hx : x = 0 then 0 else expOrderIso.symm ⟨|x|, abs_pos.2 hx⟩
