range_log

Mathlib.Analysis.SpecialFunctions.Log.Basic

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

English

The range of the real logarithm is all of ℝ.

Русский

Область значений функции логарифма равна всему множеству ℝ.

LaTeX

$$range(Real.log) = univ$$

Lean4

@[simp]
theorem range_log : range log = univ :=
  log_surjective.range_eq

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

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

Разделы

Аффилиация

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