range_logb

Mathlib.Analysis.SpecialFunctions.Log.Base

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

English

Under 0 < b and b ≠ 1, the range of log_b is all real numbers.

Русский

При 0 < b и b ≠ 1 множество значений log_b охватывает всю ℝ.

LaTeX

$$$0 < b \land b \neq 1 \Rightarrow \operatorname{range}(\log_b) = \mathbb{R}.$$$

Lean4

@[simp]
theorem range_logb : range (logb b) = univ :=
  (logb_surjective b_pos b_ne_one).range_eq

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

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

Разделы

Аффилиация

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