continuous_logb — Mathlib

English

The base-b logarithm is continuous as a function of x when x ≠ 0.

Русский

Логарифм по основанию b непрерывен как функция от x, когда x ≠ 0.

LaTeX

$$$\text{Continuous}(\log_b b\,): {x \neq 0} \to \mathbb{R}$$$

Lean4

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

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