log_surjective

Mathlib.Analysis.SpecialFunctions.Log.Basic

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

English

The logarithm function is surjective onto ℝ; for every y ∈ ℝ there exists x with log x = y.

Русский

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

LaTeX

$$Surjective(Real.log)$$

Lean4

theorem log_surjective : Surjective log := fun x => ⟨exp x, log_exp x⟩

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

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

Разделы

Аффилиация

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