surjOn_log' — Mathlib

English

The log function restricted to negative numbers is surjective onto ℝ; i.e., for every y there exists x < 0 with log x = y.

Русский

Логарифм, ограниченный отрицательными числами, сюръективен на ℝ; для каждого y существует x < 0 с log x = y.

LaTeX

$$SurjOn(Real.log, (-∞,0), ℝ)$$

Lean4

theorem surjOn_log' : SurjOn log (Iio 0) univ := fun x _ =>
  ⟨-exp x, neg_lt_zero.2 <| exp_pos x, by rw [log_neg_eq_log, log_exp]⟩

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