surjOn_log

Mathlib.Analysis.SpecialFunctions.Log.Basic

URI: https://scilib.ai/kg/mathlib#Real.surjOn_log

English

The real logarithm restricted to positive numbers is surjective onto ℝ.

Русский

Логарифм на множестве положительных чисел сюръективен на ℝ.

LaTeX

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

Lean4

theorem surjOn_log : SurjOn log (Ioi 0) univ := fun x _ => ⟨exp x, exp_pos x, log_exp x⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru