differentiableAt_log

Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

URI: https://scilib.ai/kg/mathlib#Complex.differentiableAt_log

English

The function log is differentiable at every point of the slit plane.

Русский

Функция log гладна на всей области разреза (разрезанная плоскость).

LaTeX

$$$$ \forall z \in \mathrm{slitPlane},\; \text{Differentiable}_{\mathbb{C}}(\log)(z). $$$$

Lean4

@[fun_prop]
theorem differentiableAt_log {z : ℂ} (hz : z ∈ slitPlane) : DifferentiableAt ℂ log z :=
  (hasDerivAt_log hz).differentiableAt

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

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

Разделы

Аффилиация

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