continuous_log — Mathlib

English

The real logarithm is continuous as a function on ℝ \ {0} (i.e. continuous at every nonzero point).

Русский

Действительный логарифм непрерывен на ℝ \ {0}.

LaTeX

$$$\\\\forall a \\\\ne 0, \\\\lim_{x\\\\to a} \\\\log x = \\\\log a$$$

Lean4

/-- The real logarithm is continuous as a function from nonzero reals. -/
@[fun_prop]
theorem continuous_log : Continuous fun x : { x : ℝ // x ≠ 0 } => log x :=
  continuousOn_iff_continuous_restrict.1 <| continuousOn_log.mono fun _ => id

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