continuousAt_log

Mathlib.Analysis.SpecialFunctions.Log.Basic

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

English

The log is continuous at any nonzero point: log is continuous at x if x ≠ 0.

Русский

Логарифм непрерывен в любой точке, отличной от нуля.

LaTeX

$$$\\\\forall x \\\\ne 0, \\\\lim_{h\\\\to 0} \\\\log(x+h) = \\\\log x$$$

Lean4

theorem continuousAt_log (hx : x ≠ 0) : ContinuousAt log x :=
  (continuousOn_log x hx).continuousAt <| isOpen_compl_singleton.mem_nhds hx

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

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

Разделы

Аффилиация

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