continuous_log' — Mathlib

English

The real logarithm is continuous on the positive reals: for any a>0, lim_{x→a} log x = log a.

Русский

Логарифм непрерывен на положительных числах: для любого a>0, lim_{x→a} log x = log a.

LaTeX

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

Lean4

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

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