continuous_logb' — Mathlib

English

The real base-b logarithm is continuous as a function on the positive reals.

Русский

Реальный логарифм по основанию b непрерывен на множества положительных чисел.

LaTeX

$$$\text{Continuous}_{(0,\infty)}(\log_b b)$$$

Lean4

/-- The real logarithm base b is continuous as a function from positive reals. -/
@[fun_prop]
theorem continuous_logb' : Continuous fun x : { x : ℝ // 0 < x } => logb b x :=
  continuous_log'.div_const _

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