log

Mathlib.Analysis.SpecialFunctions.Log.Deriv

URI: https://scilib.ai/kg/mathlib#ContDiffAt.log

English

If f is ContDiffAt at x and f(x) ≠ 0, then log ∘ f is ContDiffAt at x.

Русский

Если f обладает континуальной дифференцируемостью в точке x и f(x) ≠ 0, то log ∘ f дифференцируема в x.

LaTeX

$$ContDiffAt log x ∘ f$$

Lean4

@[fun_prop]
theorem log {n} (hf : ContDiffAt ℝ n f x) (hx : f x ≠ 0) : ContDiffAt ℝ n (fun x => log (f x)) x :=
  (contDiffAt_log.2 hx).comp x hf

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

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

Разделы

Аффилиация

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